open HolKernel bossLib word8Theory;

val _ = new_theory "tables";

val Sbox_def = Count.apply Define
 `(Sbox (BYTE F F F F F F F F) = BYTE F T T F F F T T) /\
  (Sbox (BYTE F F F F F F F T) = BYTE F T T T T T F F) /\
  (Sbox (BYTE F F F F F F T F) = BYTE F T T T F T T T) /\
  (Sbox (BYTE F F F F F F T T) = BYTE F T T T T F T T) /\
  (Sbox (BYTE F F F F F T F F) = BYTE T T T T F F T F) /\
  (Sbox (BYTE F F F F F T F T) = BYTE F T T F T F T T) /\
  (Sbox (BYTE F F F F F T T F) = BYTE F T T F T T T T) /\
  (Sbox (BYTE F F F F F T T T) = BYTE T T F F F T F T) /\
  (Sbox (BYTE F F F F T F F F) = BYTE F F T T F F F F) /\
  (Sbox (BYTE F F F F T F F T) = BYTE F F F F F F F T) /\
  (Sbox (BYTE F F F F T F T F) = BYTE F T T F F T T T) /\
  (Sbox (BYTE F F F F T F T T) = BYTE F F T F T F T T) /\
  (Sbox (BYTE F F F F T T F F) = BYTE T T T T T T T F) /\
  (Sbox (BYTE F F F F T T F T) = BYTE T T F T F T T T) /\
  (Sbox (BYTE F F F F T T T F) = BYTE T F T F T F T T) /\
  (Sbox (BYTE F F F F T T T T) = BYTE F T T T F T T F) /\
  (Sbox (BYTE F F F T F F F F) = BYTE T T F F T F T F) /\
  (Sbox (BYTE F F F T F F F T) = BYTE T F F F F F T F) /\
  (Sbox (BYTE F F F T F F T F) = BYTE T T F F T F F T) /\
  (Sbox (BYTE F F F T F F T T) = BYTE F T T T T T F T) /\
  (Sbox (BYTE F F F T F T F F) = BYTE T T T T T F T F) /\
  (Sbox (BYTE F F F T F T F T) = BYTE F T F T T F F T) /\
  (Sbox (BYTE F F F T F T T F) = BYTE F T F F F T T T) /\
  (Sbox (BYTE F F F T F T T T) = BYTE T T T T F F F F) /\
  (Sbox (BYTE F F F T T F F F) = BYTE T F T F T T F T) /\
  (Sbox (BYTE F F F T T F F T) = BYTE T T F T F T F F) /\
  (Sbox (BYTE F F F T T F T F) = BYTE T F T F F F T F) /\
  (Sbox (BYTE F F F T T F T T) = BYTE T F T F T T T T) /\
  (Sbox (BYTE F F F T T T F F) = BYTE T F F T T T F F) /\
  (Sbox (BYTE F F F T T T F T) = BYTE T F T F F T F F) /\
  (Sbox (BYTE F F F T T T T F) = BYTE F T T T F F T F) /\
  (Sbox (BYTE F F F T T T T T) = BYTE T T F F F F F F) /\
  (Sbox (BYTE F F T F F F F F) = BYTE T F T T F T T T) /\
  (Sbox (BYTE F F T F F F F T) = BYTE T T T T T T F T) /\
  (Sbox (BYTE F F T F F F T F) = BYTE T F F T F F T T) /\
  (Sbox (BYTE F F T F F F T T) = BYTE F F T F F T T F) /\
  (Sbox (BYTE F F T F F T F F) = BYTE F F T T F T T F) /\
  (Sbox (BYTE F F T F F T F T) = BYTE F F T T T T T T) /\
  (Sbox (BYTE F F T F F T T F) = BYTE T T T T F T T T) /\
  (Sbox (BYTE F F T F F T T T) = BYTE T T F F T T F F) /\
  (Sbox (BYTE F F T F T F F F) = BYTE F F T T F T F F) /\
  (Sbox (BYTE F F T F T F F T) = BYTE T F T F F T F T) /\
  (Sbox (BYTE F F T F T F T F) = BYTE T T T F F T F T) /\
  (Sbox (BYTE F F T F T F T T) = BYTE T T T T F F F T) /\
  (Sbox (BYTE F F T F T T F F) = BYTE F T T T F F F T) /\
  (Sbox (BYTE F F T F T T F T) = BYTE T T F T T F F F) /\
  (Sbox (BYTE F F T F T T T F) = BYTE F F T T F F F T) /\
  (Sbox (BYTE F F T F T T T T) = BYTE F F F T F T F T) /\
  (Sbox (BYTE F F T T F F F F) = BYTE F F F F F T F F) /\
  (Sbox (BYTE F F T T F F F T) = BYTE T T F F F T T T) /\
  (Sbox (BYTE F F T T F F T F) = BYTE F F T F F F T T) /\
  (Sbox (BYTE F F T T F F T T) = BYTE T T F F F F T T) /\
  (Sbox (BYTE F F T T F T F F) = BYTE F F F T T F F F) /\
  (Sbox (BYTE F F T T F T F T) = BYTE T F F T F T T F) /\
  (Sbox (BYTE F F T T F T T F) = BYTE F F F F F T F T) /\
  (Sbox (BYTE F F T T F T T T) = BYTE T F F T T F T F) /\
  (Sbox (BYTE F F T T T F F F) = BYTE F F F F F T T T) /\
  (Sbox (BYTE F F T T T F F T) = BYTE F F F T F F T F) /\
  (Sbox (BYTE F F T T T F T F) = BYTE T F F F F F F F) /\
  (Sbox (BYTE F F T T T F T T) = BYTE T T T F F F T F) /\
  (Sbox (BYTE F F T T T T F F) = BYTE T T T F T F T T) /\
  (Sbox (BYTE F F T T T T F T) = BYTE F F T F F T T T) /\
  (Sbox (BYTE F F T T T T T F) = BYTE T F T T F F T F) /\
  (Sbox (BYTE F F T T T T T T) = BYTE F T T T F T F T) /\
  (Sbox (BYTE F T F F F F F F) = BYTE F F F F T F F T) /\
  (Sbox (BYTE F T F F F F F T) = BYTE T F F F F F T T) /\
  (Sbox (BYTE F T F F F F T F) = BYTE F F T F T T F F) /\
  (Sbox (BYTE F T F F F F T T) = BYTE F F F T T F T F) /\
  (Sbox (BYTE F T F F F T F F) = BYTE F F F T T F T T) /\
  (Sbox (BYTE F T F F F T F T) = BYTE F T T F T T T F) /\
  (Sbox (BYTE F T F F F T T F) = BYTE F T F T T F T F) /\
  (Sbox (BYTE F T F F F T T T) = BYTE T F T F F F F F) /\
  (Sbox (BYTE F T F F T F F F) = BYTE F T F T F F T F) /\
  (Sbox (BYTE F T F F T F F T) = BYTE F F T T T F T T) /\
  (Sbox (BYTE F T F F T F T F) = BYTE T T F T F T T F) /\
  (Sbox (BYTE F T F F T F T T) = BYTE T F T T F F T T) /\
  (Sbox (BYTE F T F F T T F F) = BYTE F F T F T F F T) /\
  (Sbox (BYTE F T F F T T F T) = BYTE T T T F F F T T) /\
  (Sbox (BYTE F T F F T T T F) = BYTE F F T F T T T T) /\
  (Sbox (BYTE F T F F T T T T) = BYTE T F F F F T F F) /\
  (Sbox (BYTE F T F T F F F F) = BYTE F T F T F F T T) /\
  (Sbox (BYTE F T F T F F F T) = BYTE T T F T F F F T) /\
  (Sbox (BYTE F T F T F F T F) = BYTE F F F F F F F F) /\
  (Sbox (BYTE F T F T F F T T) = BYTE T T T F T T F T) /\
  (Sbox (BYTE F T F T F T F F) = BYTE F F T F F F F F) /\
  (Sbox (BYTE F T F T F T F T) = BYTE T T T T T T F F) /\
  (Sbox (BYTE F T F T F T T F) = BYTE T F T T F F F T) /\
  (Sbox (BYTE F T F T F T T T) = BYTE F T F T T F T T) /\
  (Sbox (BYTE F T F T T F F F) = BYTE F T T F T F T F) /\
  (Sbox (BYTE F T F T T F F T) = BYTE T T F F T F T T) /\
  (Sbox (BYTE F T F T T F T F) = BYTE T F T T T T T F) /\
  (Sbox (BYTE F T F T T F T T) = BYTE F F T T T F F T) /\
  (Sbox (BYTE F T F T T T F F) = BYTE F T F F T F T F) /\
  (Sbox (BYTE F T F T T T F T) = BYTE F T F F T T F F) /\
  (Sbox (BYTE F T F T T T T F) = BYTE F T F T T F F F) /\
  (Sbox (BYTE F T F T T T T T) = BYTE T T F F T T T T) /\
  (Sbox (BYTE F T T F F F F F) = BYTE T T F T F F F F) /\
  (Sbox (BYTE F T T F F F F T) = BYTE T T T F T T T T) /\
  (Sbox (BYTE F T T F F F T F) = BYTE T F T F T F T F) /\
  (Sbox (BYTE F T T F F F T T) = BYTE T T T T T F T T) /\
  (Sbox (BYTE F T T F F T F F) = BYTE F T F F F F T T) /\
  (Sbox (BYTE F T T F F T F T) = BYTE F T F F T T F T) /\
  (Sbox (BYTE F T T F F T T F) = BYTE F F T T F F T T) /\
  (Sbox (BYTE F T T F F T T T) = BYTE T F F F F T F T) /\
  (Sbox (BYTE F T T F T F F F) = BYTE F T F F F T F T) /\
  (Sbox (BYTE F T T F T F F T) = BYTE T T T T T F F T) /\
  (Sbox (BYTE F T T F T F T F) = BYTE F F F F F F T F) /\
  (Sbox (BYTE F T T F T F T T) = BYTE F T T T T T T T) /\
  (Sbox (BYTE F T T F T T F F) = BYTE F T F T F F F F) /\
  (Sbox (BYTE F T T F T T F T) = BYTE F F T T T T F F) /\
  (Sbox (BYTE F T T F T T T F) = BYTE T F F T T T T T) /\
  (Sbox (BYTE F T T F T T T T) = BYTE T F T F T F F F) /\
  (Sbox (BYTE F T T T F F F F) = BYTE F T F T F F F T) /\
  (Sbox (BYTE F T T T F F F T) = BYTE T F T F F F T T) /\
  (Sbox (BYTE F T T T F F T F) = BYTE F T F F F F F F) /\
  (Sbox (BYTE F T T T F F T T) = BYTE T F F F T T T T) /\
  (Sbox (BYTE F T T T F T F F) = BYTE T F F T F F T F) /\
  (Sbox (BYTE F T T T F T F T) = BYTE T F F T T T F T) /\
  (Sbox (BYTE F T T T F T T F) = BYTE F F T T T F F F) /\
  (Sbox (BYTE F T T T F T T T) = BYTE T T T T F T F T) /\
  (Sbox (BYTE F T T T T F F F) = BYTE T F T T T T F F) /\
  (Sbox (BYTE F T T T T F F T) = BYTE T F T T F T T F) /\
  (Sbox (BYTE F T T T T F T F) = BYTE T T F T T F T F) /\
  (Sbox (BYTE F T T T T F T T) = BYTE F F T F F F F T) /\
  (Sbox (BYTE F T T T T T F F) = BYTE F F F T F F F F) /\
  (Sbox (BYTE F T T T T T F T) = BYTE T T T T T T T T) /\
  (Sbox (BYTE F T T T T T T F) = BYTE T T T T F F T T) /\
  (Sbox (BYTE F T T T T T T T) = BYTE T T F T F F T F) /\
  (Sbox (BYTE T F F F F F F F) = BYTE T T F F T T F T) /\
  (Sbox (BYTE T F F F F F F T) = BYTE F F F F T T F F) /\
  (Sbox (BYTE T F F F F F T F) = BYTE F F F T F F T T) /\
  (Sbox (BYTE T F F F F F T T) = BYTE T T T F T T F F) /\
  (Sbox (BYTE T F F F F T F F) = BYTE F T F T T T T T) /\
  (Sbox (BYTE T F F F F T F T) = BYTE T F F T F T T T) /\
  (Sbox (BYTE T F F F F T T F) = BYTE F T F F F T F F) /\
  (Sbox (BYTE T F F F F T T T) = BYTE F F F T F T T T) /\
  (Sbox (BYTE T F F F T F F F) = BYTE T T F F F T F F) /\
  (Sbox (BYTE T F F F T F F T) = BYTE T F T F F T T T) /\
  (Sbox (BYTE T F F F T F T F) = BYTE F T T T T T T F) /\
  (Sbox (BYTE T F F F T F T T) = BYTE F F T T T T F T) /\
  (Sbox (BYTE T F F F T T F F) = BYTE F T T F F T F F) /\
  (Sbox (BYTE T F F F T T F T) = BYTE F T F T T T F T) /\
  (Sbox (BYTE T F F F T T T F) = BYTE F F F T T F F T) /\
  (Sbox (BYTE T F F F T T T T) = BYTE F T T T F F T T) /\
  (Sbox (BYTE T F F T F F F F) = BYTE F T T F F F F F) /\
  (Sbox (BYTE T F F T F F F T) = BYTE T F F F F F F T) /\
  (Sbox (BYTE T F F T F F T F) = BYTE F T F F T T T T) /\
  (Sbox (BYTE T F F T F F T T) = BYTE T T F T T T F F) /\
  (Sbox (BYTE T F F T F T F F) = BYTE F F T F F F T F) /\
  (Sbox (BYTE T F F T F T F T) = BYTE F F T F T F T F) /\
  (Sbox (BYTE T F F T F T T F) = BYTE T F F T F F F F) /\
  (Sbox (BYTE T F F T F T T T) = BYTE T F F F T F F F) /\
  (Sbox (BYTE T F F T T F F F) = BYTE F T F F F T T F) /\
  (Sbox (BYTE T F F T T F F T) = BYTE T T T F T T T F) /\
  (Sbox (BYTE T F F T T F T F) = BYTE T F T T T F F F) /\
  (Sbox (BYTE T F F T T F T T) = BYTE F F F T F T F F) /\
  (Sbox (BYTE T F F T T T F F) = BYTE T T F T T T T F) /\
  (Sbox (BYTE T F F T T T F T) = BYTE F T F T T T T F) /\
  (Sbox (BYTE T F F T T T T F) = BYTE F F F F T F T T) /\
  (Sbox (BYTE T F F T T T T T) = BYTE T T F T T F T T) /\
  (Sbox (BYTE T F T F F F F F) = BYTE T T T F F F F F) /\
  (Sbox (BYTE T F T F F F F T) = BYTE F F T T F F T F) /\
  (Sbox (BYTE T F T F F F T F) = BYTE F F T T T F T F) /\
  (Sbox (BYTE T F T F F F T T) = BYTE F F F F T F T F) /\
  (Sbox (BYTE T F T F F T F F) = BYTE F T F F T F F T) /\
  (Sbox (BYTE T F T F F T F T) = BYTE F F F F F T T F) /\
  (Sbox (BYTE T F T F F T T F) = BYTE F F T F F T F F) /\
  (Sbox (BYTE T F T F F T T T) = BYTE F T F T T T F F) /\
  (Sbox (BYTE T F T F T F F F) = BYTE T T F F F F T F) /\
  (Sbox (BYTE T F T F T F F T) = BYTE T T F T F F T T) /\
  (Sbox (BYTE T F T F T F T F) = BYTE T F T F T T F F) /\
  (Sbox (BYTE T F T F T F T T) = BYTE F T T F F F T F) /\
  (Sbox (BYTE T F T F T T F F) = BYTE T F F T F F F T) /\
  (Sbox (BYTE T F T F T T F T) = BYTE T F F T F T F T) /\
  (Sbox (BYTE T F T F T T T F) = BYTE T T T F F T F F) /\
  (Sbox (BYTE T F T F T T T T) = BYTE F T T T T F F T) /\
  (Sbox (BYTE T F T T F F F F) = BYTE T T T F F T T T) /\
  (Sbox (BYTE T F T T F F F T) = BYTE T T F F T F F F) /\
  (Sbox (BYTE T F T T F F T F) = BYTE F F T T F T T T) /\
  (Sbox (BYTE T F T T F F T T) = BYTE F T T F T T F T) /\
  (Sbox (BYTE T F T T F T F F) = BYTE T F F F T T F T) /\
  (Sbox (BYTE T F T T F T F T) = BYTE T T F T F T F T) /\
  (Sbox (BYTE T F T T F T T F) = BYTE F T F F T T T F) /\
  (Sbox (BYTE T F T T F T T T) = BYTE T F T F T F F T) /\
  (Sbox (BYTE T F T T T F F F) = BYTE F T T F T T F F) /\
  (Sbox (BYTE T F T T T F F T) = BYTE F T F T F T T F) /\
  (Sbox (BYTE T F T T T F T F) = BYTE T T T T F T F F) /\
  (Sbox (BYTE T F T T T F T T) = BYTE T T T F T F T F) /\
  (Sbox (BYTE T F T T T T F F) = BYTE F T T F F T F T) /\
  (Sbox (BYTE T F T T T T F T) = BYTE F T T T T F T F) /\
  (Sbox (BYTE T F T T T T T F) = BYTE T F T F T T T F) /\
  (Sbox (BYTE T F T T T T T T) = BYTE F F F F T F F F) /\
  (Sbox (BYTE T T F F F F F F) = BYTE T F T T T F T F) /\
  (Sbox (BYTE T T F F F F F T) = BYTE F T T T T F F F) /\
  (Sbox (BYTE T T F F F F T F) = BYTE F F T F F T F T) /\
  (Sbox (BYTE T T F F F F T T) = BYTE F F T F T T T F) /\
  (Sbox (BYTE T T F F F T F F) = BYTE F F F T T T F F) /\
  (Sbox (BYTE T T F F F T F T) = BYTE T F T F F T T F) /\
  (Sbox (BYTE T T F F F T T F) = BYTE T F T T F T F F) /\
  (Sbox (BYTE T T F F F T T T) = BYTE T T F F F T T F) /\
  (Sbox (BYTE T T F F T F F F) = BYTE T T T F T F F F) /\
  (Sbox (BYTE T T F F T F F T) = BYTE T T F T T T F T) /\
  (Sbox (BYTE T T F F T F T F) = BYTE F T T T F T F F) /\
  (Sbox (BYTE T T F F T F T T) = BYTE F F F T T T T T) /\
  (Sbox (BYTE T T F F T T F F) = BYTE F T F F T F T T) /\
  (Sbox (BYTE T T F F T T F T) = BYTE T F T T T T F T) /\
  (Sbox (BYTE T T F F T T T F) = BYTE T F F F T F T T) /\
  (Sbox (BYTE T T F F T T T T) = BYTE T F F F T F T F) /\
  (Sbox (BYTE T T F T F F F F) = BYTE F T T T F F F F) /\
  (Sbox (BYTE T T F T F F F T) = BYTE F F T T T T T F) /\
  (Sbox (BYTE T T F T F F T F) = BYTE T F T T F T F T) /\
  (Sbox (BYTE T T F T F F T T) = BYTE F T T F F T T F) /\
  (Sbox (BYTE T T F T F T F F) = BYTE F T F F T F F F) /\
  (Sbox (BYTE T T F T F T F T) = BYTE F F F F F F T T) /\
  (Sbox (BYTE T T F T F T T F) = BYTE T T T T F T T F) /\
  (Sbox (BYTE T T F T F T T T) = BYTE F F F F T T T F) /\
  (Sbox (BYTE T T F T T F F F) = BYTE F T T F F F F T) /\
  (Sbox (BYTE T T F T T F F T) = BYTE F F T T F T F T) /\
  (Sbox (BYTE T T F T T F T F) = BYTE F T F T F T T T) /\
  (Sbox (BYTE T T F T T F T T) = BYTE T F T T T F F T) /\
  (Sbox (BYTE T T F T T T F F) = BYTE T F F F F T T F) /\
  (Sbox (BYTE T T F T T T F T) = BYTE T T F F F F F T) /\
  (Sbox (BYTE T T F T T T T F) = BYTE F F F T T T F T) /\
  (Sbox (BYTE T T F T T T T T) = BYTE T F F T T T T F) /\
  (Sbox (BYTE T T T F F F F F) = BYTE T T T F F F F T) /\
  (Sbox (BYTE T T T F F F F T) = BYTE T T T T T F F F) /\
  (Sbox (BYTE T T T F F F T F) = BYTE T F F T T F F F) /\
  (Sbox (BYTE T T T F F F T T) = BYTE F F F T F F F T) /\
  (Sbox (BYTE T T T F F T F F) = BYTE F T T F T F F T) /\
  (Sbox (BYTE T T T F F T F T) = BYTE T T F T T F F T) /\
  (Sbox (BYTE T T T F F T T F) = BYTE T F F F T T T F) /\
  (Sbox (BYTE T T T F F T T T) = BYTE T F F T F T F F) /\
  (Sbox (BYTE T T T F T F F F) = BYTE T F F T T F T T) /\
  (Sbox (BYTE T T T F T F F T) = BYTE F F F T T T T F) /\
  (Sbox (BYTE T T T F T F T F) = BYTE T F F F F T T T) /\
  (Sbox (BYTE T T T F T F T T) = BYTE T T T F T F F T) /\
  (Sbox (BYTE T T T F T T F F) = BYTE T T F F T T T F) /\
  (Sbox (BYTE T T T F T T F T) = BYTE F T F T F T F T) /\
  (Sbox (BYTE T T T F T T T F) = BYTE F F T F T F F F) /\
  (Sbox (BYTE T T T F T T T T) = BYTE T T F T T T T T) /\
  (Sbox (BYTE T T T T F F F F) = BYTE T F F F T T F F) /\
  (Sbox (BYTE T T T T F F F T) = BYTE T F T F F F F T) /\
  (Sbox (BYTE T T T T F F T F) = BYTE T F F F T F F T) /\
  (Sbox (BYTE T T T T F F T T) = BYTE F F F F T T F T) /\
  (Sbox (BYTE T T T T F T F F) = BYTE T F T T T T T T) /\
  (Sbox (BYTE T T T T F T F T) = BYTE T T T F F T T F) /\
  (Sbox (BYTE T T T T F T T F) = BYTE F T F F F F T F) /\
  (Sbox (BYTE T T T T F T T T) = BYTE F T T F T F F F) /\
  (Sbox (BYTE T T T T T F F F) = BYTE F T F F F F F T) /\
  (Sbox (BYTE T T T T T F F T) = BYTE T F F T T F F T) /\
  (Sbox (BYTE T T T T T F T F) = BYTE F F T F T T F T) /\
  (Sbox (BYTE T T T T T F T T) = BYTE F F F F T T T T) /\
  (Sbox (BYTE T T T T T T F F) = BYTE T F T T F F F F) /\
  (Sbox (BYTE T T T T T T F T) = BYTE F T F T F T F F) /\
  (Sbox (BYTE T T T T T T T F) = BYTE T F T T T F T T) /\
  (Sbox (BYTE T T T T T T T T) = BYTE F F F T F T T F)`;

val InvSbox_def = Count.apply Define
 `(InvSbox (BYTE F F F F F F F F) = BYTE F T F T F F T F) /\
  (InvSbox (BYTE F F F F F F F T) = BYTE F F F F T F F T) /\
  (InvSbox (BYTE F F F F F F T F) = BYTE F T T F T F T F) /\
  (InvSbox (BYTE F F F F F F T T) = BYTE T T F T F T F T) /\
  (InvSbox (BYTE F F F F F T F F) = BYTE F F T T F F F F) /\
  (InvSbox (BYTE F F F F F T F T) = BYTE F F T T F T T F) /\
  (InvSbox (BYTE F F F F F T T F) = BYTE T F T F F T F T) /\
  (InvSbox (BYTE F F F F F T T T) = BYTE F F T T T F F F) /\
  (InvSbox (BYTE F F F F T F F F) = BYTE T F T T T T T T) /\
  (InvSbox (BYTE F F F F T F F T) = BYTE F T F F F F F F) /\
  (InvSbox (BYTE F F F F T F T F) = BYTE T F T F F F T T) /\
  (InvSbox (BYTE F F F F T F T T) = BYTE T F F T T T T F) /\
  (InvSbox (BYTE F F F F T T F F) = BYTE T F F F F F F T) /\
  (InvSbox (BYTE F F F F T T F T) = BYTE T T T T F F T T) /\
  (InvSbox (BYTE F F F F T T T F) = BYTE T T F T F T T T) /\
  (InvSbox (BYTE F F F F T T T T) = BYTE T T T T T F T T) /\
  (InvSbox (BYTE F F F T F F F F) = BYTE F T T T T T F F) /\
  (InvSbox (BYTE F F F T F F F T) = BYTE T T T F F F T T) /\
  (InvSbox (BYTE F F F T F F T F) = BYTE F F T T T F F T) /\
  (InvSbox (BYTE F F F T F F T T) = BYTE T F F F F F T F) /\
  (InvSbox (BYTE F F F T F T F F) = BYTE T F F T T F T T) /\
  (InvSbox (BYTE F F F T F T F T) = BYTE F F T F T T T T) /\
  (InvSbox (BYTE F F F T F T T F) = BYTE T T T T T T T T) /\
  (InvSbox (BYTE F F F T F T T T) = BYTE T F F F F T T T) /\
  (InvSbox (BYTE F F F T T F F F) = BYTE F F T T F T F F) /\
  (InvSbox (BYTE F F F T T F F T) = BYTE T F F F T T T F) /\
  (InvSbox (BYTE F F F T T F T F) = BYTE F T F F F F T T) /\
  (InvSbox (BYTE F F F T T F T T) = BYTE F T F F F T F F) /\
  (InvSbox (BYTE F F F T T T F F) = BYTE T T F F F T F F) /\
  (InvSbox (BYTE F F F T T T F T) = BYTE T T F T T T T F) /\
  (InvSbox (BYTE F F F T T T T F) = BYTE T T T F T F F T) /\
  (InvSbox (BYTE F F F T T T T T) = BYTE T T F F T F T T) /\
  (InvSbox (BYTE F F T F F F F F) = BYTE F T F T F T F F) /\
  (InvSbox (BYTE F F T F F F F T) = BYTE F T T T T F T T) /\
  (InvSbox (BYTE F F T F F F T F) = BYTE T F F T F T F F) /\
  (InvSbox (BYTE F F T F F F T T) = BYTE F F T T F F T F) /\
  (InvSbox (BYTE F F T F F T F F) = BYTE T F T F F T T F) /\
  (InvSbox (BYTE F F T F F T F T) = BYTE T T F F F F T F) /\
  (InvSbox (BYTE F F T F F T T F) = BYTE F F T F F F T T) /\
  (InvSbox (BYTE F F T F F T T T) = BYTE F F T T T T F T) /\
  (InvSbox (BYTE F F T F T F F F) = BYTE T T T F T T T F) /\
  (InvSbox (BYTE F F T F T F F T) = BYTE F T F F T T F F) /\
  (InvSbox (BYTE F F T F T F T F) = BYTE T F F T F T F T) /\
  (InvSbox (BYTE F F T F T F T T) = BYTE F F F F T F T T) /\
  (InvSbox (BYTE F F T F T T F F) = BYTE F T F F F F T F) /\
  (InvSbox (BYTE F F T F T T F T) = BYTE T T T T T F T F) /\
  (InvSbox (BYTE F F T F T T T F) = BYTE T T F F F F T T) /\
  (InvSbox (BYTE F F T F T T T T) = BYTE F T F F T T T F) /\
  (InvSbox (BYTE F F T T F F F F) = BYTE F F F F T F F F) /\
  (InvSbox (BYTE F F T T F F F T) = BYTE F F T F T T T F) /\
  (InvSbox (BYTE F F T T F F T F) = BYTE T F T F F F F T) /\
  (InvSbox (BYTE F F T T F F T T) = BYTE F T T F F T T F) /\
  (InvSbox (BYTE F F T T F T F F) = BYTE F F T F T F F F) /\
  (InvSbox (BYTE F F T T F T F T) = BYTE T T F T T F F T) /\
  (InvSbox (BYTE F F T T F T T F) = BYTE F F T F F T F F) /\
  (InvSbox (BYTE F F T T F T T T) = BYTE T F T T F F T F) /\
  (InvSbox (BYTE F F T T T F F F) = BYTE F T T T F T T F) /\
  (InvSbox (BYTE F F T T T F F T) = BYTE F T F T T F T T) /\
  (InvSbox (BYTE F F T T T F T F) = BYTE T F T F F F T F) /\
  (InvSbox (BYTE F F T T T F T T) = BYTE F T F F T F F T) /\
  (InvSbox (BYTE F F T T T T F F) = BYTE F T T F T T F T) /\
  (InvSbox (BYTE F F T T T T F T) = BYTE T F F F T F T T) /\
  (InvSbox (BYTE F F T T T T T F) = BYTE T T F T F F F T) /\
  (InvSbox (BYTE F F T T T T T T) = BYTE F F T F F T F T) /\
  (InvSbox (BYTE F T F F F F F F) = BYTE F T T T F F T F) /\
  (InvSbox (BYTE F T F F F F F T) = BYTE T T T T T F F F) /\
  (InvSbox (BYTE F T F F F F T F) = BYTE T T T T F T T F) /\
  (InvSbox (BYTE F T F F F F T T) = BYTE F T T F F T F F) /\
  (InvSbox (BYTE F T F F F T F F) = BYTE T F F F F T T F) /\
  (InvSbox (BYTE F T F F F T F T) = BYTE F T T F T F F F) /\
  (InvSbox (BYTE F T F F F T T F) = BYTE T F F T T F F F) /\
  (InvSbox (BYTE F T F F F T T T) = BYTE F F F T F T T F) /\
  (InvSbox (BYTE F T F F T F F F) = BYTE T T F T F T F F) /\
  (InvSbox (BYTE F T F F T F F T) = BYTE T F T F F T F F) /\
  (InvSbox (BYTE F T F F T F T F) = BYTE F T F T T T F F) /\
  (InvSbox (BYTE F T F F T F T T) = BYTE T T F F T T F F) /\
  (InvSbox (BYTE F T F F T T F F) = BYTE F T F T T T F T) /\
  (InvSbox (BYTE F T F F T T F T) = BYTE F T T F F T F T) /\
  (InvSbox (BYTE F T F F T T T F) = BYTE T F T T F T T F) /\
  (InvSbox (BYTE F T F F T T T T) = BYTE T F F T F F T F) /\
  (InvSbox (BYTE F T F T F F F F) = BYTE F T T F T T F F) /\
  (InvSbox (BYTE F T F T F F F T) = BYTE F T T T F F F F) /\
  (InvSbox (BYTE F T F T F F T F) = BYTE F T F F T F F F) /\
  (InvSbox (BYTE F T F T F F T T) = BYTE F T F T F F F F) /\
  (InvSbox (BYTE F T F T F T F F) = BYTE T T T T T T F T) /\
  (InvSbox (BYTE F T F T F T F T) = BYTE T T T F T T F T) /\
  (InvSbox (BYTE F T F T F T T F) = BYTE T F T T T F F T) /\
  (InvSbox (BYTE F T F T F T T T) = BYTE T T F T T F T F) /\
  (InvSbox (BYTE F T F T T F F F) = BYTE F T F T T T T F) /\
  (InvSbox (BYTE F T F T T F F T) = BYTE F F F T F T F T) /\
  (InvSbox (BYTE F T F T T F T F) = BYTE F T F F F T T F) /\
  (InvSbox (BYTE F T F T T F T T) = BYTE F T F T F T T T) /\
  (InvSbox (BYTE F T F T T T F F) = BYTE T F T F F T T T) /\
  (InvSbox (BYTE F T F T T T F T) = BYTE T F F F T T F T) /\
  (InvSbox (BYTE F T F T T T T F) = BYTE T F F T T T F T) /\
  (InvSbox (BYTE F T F T T T T T) = BYTE T F F F F T F F) /\
  (InvSbox (BYTE F T T F F F F F) = BYTE T F F T F F F F) /\
  (InvSbox (BYTE F T T F F F F T) = BYTE T T F T T F F F) /\
  (InvSbox (BYTE F T T F F F T F) = BYTE T F T F T F T T) /\
  (InvSbox (BYTE F T T F F F T T) = BYTE F F F F F F F F) /\
  (InvSbox (BYTE F T T F F T F F) = BYTE T F F F T T F F) /\
  (InvSbox (BYTE F T T F F T F T) = BYTE T F T T T T F F) /\
  (InvSbox (BYTE F T T F F T T F) = BYTE T T F T F F T T) /\
  (InvSbox (BYTE F T T F F T T T) = BYTE F F F F T F T F) /\
  (InvSbox (BYTE F T T F T F F F) = BYTE T T T T F T T T) /\
  (InvSbox (BYTE F T T F T F F T) = BYTE T T T F F T F F) /\
  (InvSbox (BYTE F T T F T F T F) = BYTE F T F T T F F F) /\
  (InvSbox (BYTE F T T F T F T T) = BYTE F F F F F T F T) /\
  (InvSbox (BYTE F T T F T T F F) = BYTE T F T T T F F F) /\
  (InvSbox (BYTE F T T F T T F T) = BYTE T F T T F F T T) /\
  (InvSbox (BYTE F T T F T T T F) = BYTE F T F F F T F T) /\
  (InvSbox (BYTE F T T F T T T T) = BYTE F F F F F T T F) /\
  (InvSbox (BYTE F T T T F F F F) = BYTE T T F T F F F F) /\
  (InvSbox (BYTE F T T T F F F T) = BYTE F F T F T T F F) /\
  (InvSbox (BYTE F T T T F F T F) = BYTE F F F T T T T F) /\
  (InvSbox (BYTE F T T T F F T T) = BYTE T F F F T T T T) /\
  (InvSbox (BYTE F T T T F T F F) = BYTE T T F F T F T F) /\
  (InvSbox (BYTE F T T T F T F T) = BYTE F F T T T T T T) /\
  (InvSbox (BYTE F T T T F T T F) = BYTE F F F F T T T T) /\
  (InvSbox (BYTE F T T T F T T T) = BYTE F F F F F F T F) /\
  (InvSbox (BYTE F T T T T F F F) = BYTE T T F F F F F T) /\
  (InvSbox (BYTE F T T T T F F T) = BYTE T F T F T T T T) /\
  (InvSbox (BYTE F T T T T F T F) = BYTE T F T T T T F T) /\
  (InvSbox (BYTE F T T T T F T T) = BYTE F F F F F F T T) /\
  (InvSbox (BYTE F T T T T T F F) = BYTE F F F F F F F T) /\
  (InvSbox (BYTE F T T T T T F T) = BYTE F F F T F F T T) /\
  (InvSbox (BYTE F T T T T T T F) = BYTE T F F F T F T F) /\
  (InvSbox (BYTE F T T T T T T T) = BYTE F T T F T F T T) /\
  (InvSbox (BYTE T F F F F F F F) = BYTE F F T T T F T F) /\
  (InvSbox (BYTE T F F F F F F T) = BYTE T F F T F F F T) /\
  (InvSbox (BYTE T F F F F F T F) = BYTE F F F T F F F T) /\
  (InvSbox (BYTE T F F F F F T T) = BYTE F T F F F F F T) /\
  (InvSbox (BYTE T F F F F T F F) = BYTE F T F F T T T T) /\
  (InvSbox (BYTE T F F F F T F T) = BYTE F T T F F T T T) /\
  (InvSbox (BYTE T F F F F T T F) = BYTE T T F T T T F F) /\
  (InvSbox (BYTE T F F F F T T T) = BYTE T T T F T F T F) /\
  (InvSbox (BYTE T F F F T F F F) = BYTE T F F T F T T T) /\
  (InvSbox (BYTE T F F F T F F T) = BYTE T T T T F F T F) /\
  (InvSbox (BYTE T F F F T F T F) = BYTE T T F F T T T T) /\
  (InvSbox (BYTE T F F F T F T T) = BYTE T T F F T T T F) /\
  (InvSbox (BYTE T F F F T T F F) = BYTE T T T T F F F F) /\
  (InvSbox (BYTE T F F F T T F T) = BYTE T F T T F T F F) /\
  (InvSbox (BYTE T F F F T T T F) = BYTE T T T F F T T F) /\
  (InvSbox (BYTE T F F F T T T T) = BYTE F T T T F F T T) /\
  (InvSbox (BYTE T F F T F F F F) = BYTE T F F T F T T F) /\
  (InvSbox (BYTE T F F T F F F T) = BYTE T F T F T T F F) /\
  (InvSbox (BYTE T F F T F F T F) = BYTE F T T T F T F F) /\
  (InvSbox (BYTE T F F T F F T T) = BYTE F F T F F F T F) /\
  (InvSbox (BYTE T F F T F T F F) = BYTE T T T F F T T T) /\
  (InvSbox (BYTE T F F T F T F T) = BYTE T F T F T T F T) /\
  (InvSbox (BYTE T F F T F T T F) = BYTE F F T T F T F T) /\
  (InvSbox (BYTE T F F T F T T T) = BYTE T F F F F T F T) /\
  (InvSbox (BYTE T F F T T F F F) = BYTE T T T F F F T F) /\
  (InvSbox (BYTE T F F T T F F T) = BYTE T T T T T F F T) /\
  (InvSbox (BYTE T F F T T F T F) = BYTE F F T T F T T T) /\
  (InvSbox (BYTE T F F T T F T T) = BYTE T T T F T F F F) /\
  (InvSbox (BYTE T F F T T T F F) = BYTE F F F T T T F F) /\
  (InvSbox (BYTE T F F T T T F T) = BYTE F T T T F T F T) /\
  (InvSbox (BYTE T F F T T T T F) = BYTE T T F T T T T T) /\
  (InvSbox (BYTE T F F T T T T T) = BYTE F T T F T T T F) /\
  (InvSbox (BYTE T F T F F F F F) = BYTE F T F F F T T T) /\
  (InvSbox (BYTE T F T F F F F T) = BYTE T T T T F F F T) /\
  (InvSbox (BYTE T F T F F F T F) = BYTE F F F T T F T F) /\
  (InvSbox (BYTE T F T F F F T T) = BYTE F T T T F F F T) /\
  (InvSbox (BYTE T F T F F T F F) = BYTE F F F T T T F T) /\
  (InvSbox (BYTE T F T F F T F T) = BYTE F F T F T F F T) /\
  (InvSbox (BYTE T F T F F T T F) = BYTE T T F F F T F T) /\
  (InvSbox (BYTE T F T F F T T T) = BYTE T F F F T F F T) /\
  (InvSbox (BYTE T F T F T F F F) = BYTE F T T F T T T T) /\
  (InvSbox (BYTE T F T F T F F T) = BYTE T F T T F T T T) /\
  (InvSbox (BYTE T F T F T F T F) = BYTE F T T F F F T F) /\
  (InvSbox (BYTE T F T F T F T T) = BYTE F F F F T T T F) /\
  (InvSbox (BYTE T F T F T T F F) = BYTE T F T F T F T F) /\
  (InvSbox (BYTE T F T F T T F T) = BYTE F F F T T F F F) /\
  (InvSbox (BYTE T F T F T T T F) = BYTE T F T T T T T F) /\
  (InvSbox (BYTE T F T F T T T T) = BYTE F F F T T F T T) /\
  (InvSbox (BYTE T F T T F F F F) = BYTE T T T T T T F F) /\
  (InvSbox (BYTE T F T T F F F T) = BYTE F T F T F T T F) /\
  (InvSbox (BYTE T F T T F F T F) = BYTE F F T T T T T F) /\
  (InvSbox (BYTE T F T T F F T T) = BYTE F T F F T F T T) /\
  (InvSbox (BYTE T F T T F T F F) = BYTE T T F F F T T F) /\
  (InvSbox (BYTE T F T T F T F T) = BYTE T T F T F F T F) /\
  (InvSbox (BYTE T F T T F T T F) = BYTE F T T T T F F T) /\
  (InvSbox (BYTE T F T T F T T T) = BYTE F F T F F F F F) /\
  (InvSbox (BYTE T F T T T F F F) = BYTE T F F T T F T F) /\
  (InvSbox (BYTE T F T T T F F T) = BYTE T T F T T F T T) /\
  (InvSbox (BYTE T F T T T F T F) = BYTE T T F F F F F F) /\
  (InvSbox (BYTE T F T T T F T T) = BYTE T T T T T T T F) /\
  (InvSbox (BYTE T F T T T T F F) = BYTE F T T T T F F F) /\
  (InvSbox (BYTE T F T T T T F T) = BYTE T T F F T T F T) /\
  (InvSbox (BYTE T F T T T T T F) = BYTE F T F T T F T F) /\
  (InvSbox (BYTE T F T T T T T T) = BYTE T T T T F T F F) /\
  (InvSbox (BYTE T T F F F F F F) = BYTE F F F T T T T T) /\
  (InvSbox (BYTE T T F F F F F T) = BYTE T T F T T T F T) /\
  (InvSbox (BYTE T T F F F F T F) = BYTE T F T F T F F F) /\
  (InvSbox (BYTE T T F F F F T T) = BYTE F F T T F F T T) /\
  (InvSbox (BYTE T T F F F T F F) = BYTE T F F F T F F F) /\
  (InvSbox (BYTE T T F F F T F T) = BYTE F F F F F T T T) /\
  (InvSbox (BYTE T T F F F T T F) = BYTE T T F F F T T T) /\
  (InvSbox (BYTE T T F F F T T T) = BYTE F F T T F F F T) /\
  (InvSbox (BYTE T T F F T F F F) = BYTE T F T T F F F T) /\
  (InvSbox (BYTE T T F F T F F T) = BYTE F F F T F F T F) /\
  (InvSbox (BYTE T T F F T F T F) = BYTE F F F T F F F F) /\
  (InvSbox (BYTE T T F F T F T T) = BYTE F T F T T F F T) /\
  (InvSbox (BYTE T T F F T T F F) = BYTE F F T F F T T T) /\
  (InvSbox (BYTE T T F F T T F T) = BYTE T F F F F F F F) /\
  (InvSbox (BYTE T T F F T T T F) = BYTE T T T F T T F F) /\
  (InvSbox (BYTE T T F F T T T T) = BYTE F T F T T T T T) /\
  (InvSbox (BYTE T T F T F F F F) = BYTE F T T F F F F F) /\
  (InvSbox (BYTE T T F T F F F T) = BYTE F T F T F F F T) /\
  (InvSbox (BYTE T T F T F F T F) = BYTE F T T T T T T T) /\
  (InvSbox (BYTE T T F T F F T T) = BYTE T F T F T F F T) /\
  (InvSbox (BYTE T T F T F T F F) = BYTE F F F T T F F T) /\
  (InvSbox (BYTE T T F T F T F T) = BYTE T F T T F T F T) /\
  (InvSbox (BYTE T T F T F T T F) = BYTE F T F F T F T F) /\
  (InvSbox (BYTE T T F T F T T T) = BYTE F F F F T T F T) /\
  (InvSbox (BYTE T T F T T F F F) = BYTE F F T F T T F T) /\
  (InvSbox (BYTE T T F T T F F T) = BYTE T T T F F T F T) /\
  (InvSbox (BYTE T T F T T F T F) = BYTE F T T T T F T F) /\
  (InvSbox (BYTE T T F T T F T T) = BYTE T F F T T T T T) /\
  (InvSbox (BYTE T T F T T T F F) = BYTE T F F T F F T T) /\
  (InvSbox (BYTE T T F T T T F T) = BYTE T T F F T F F T) /\
  (InvSbox (BYTE T T F T T T T F) = BYTE T F F T T T F F) /\
  (InvSbox (BYTE T T F T T T T T) = BYTE T T T F T T T T) /\
  (InvSbox (BYTE T T T F F F F F) = BYTE T F T F F F F F) /\
  (InvSbox (BYTE T T T F F F F T) = BYTE T T T F F F F F) /\
  (InvSbox (BYTE T T T F F F T F) = BYTE F F T T T F T T) /\
  (InvSbox (BYTE T T T F F F T T) = BYTE F T F F T T F T) /\
  (InvSbox (BYTE T T T F F T F F) = BYTE T F T F T T T F) /\
  (InvSbox (BYTE T T T F F T F T) = BYTE F F T F T F T F) /\
  (InvSbox (BYTE T T T F F T T F) = BYTE T T T T F T F T) /\
  (InvSbox (BYTE T T T F F T T T) = BYTE T F T T F F F F) /\
  (InvSbox (BYTE T T T F T F F F) = BYTE T T F F T F F F) /\
  (InvSbox (BYTE T T T F T F F T) = BYTE T T T F T F T T) /\
  (InvSbox (BYTE T T T F T F T F) = BYTE T F T T T F T T) /\
  (InvSbox (BYTE T T T F T F T T) = BYTE F F T T T T F F) /\
  (InvSbox (BYTE T T T F T T F F) = BYTE T F F F F F T T) /\
  (InvSbox (BYTE T T T F T T F T) = BYTE F T F T F F T T) /\
  (InvSbox (BYTE T T T F T T T F) = BYTE T F F T T F F T) /\
  (InvSbox (BYTE T T T F T T T T) = BYTE F T T F F F F T) /\
  (InvSbox (BYTE T T T T F F F F) = BYTE F F F T F T T T) /\
  (InvSbox (BYTE T T T T F F F T) = BYTE F F T F T F T T) /\
  (InvSbox (BYTE T T T T F F T F) = BYTE F F F F F T F F) /\
  (InvSbox (BYTE T T T T F F T T) = BYTE F T T T T T T F) /\
  (InvSbox (BYTE T T T T F T F F) = BYTE T F T T T F T F) /\
  (InvSbox (BYTE T T T T F T F T) = BYTE F T T T F T T T) /\
  (InvSbox (BYTE T T T T F T T F) = BYTE T T F T F T T F) /\
  (InvSbox (BYTE T T T T F T T T) = BYTE F F T F F T T F) /\
  (InvSbox (BYTE T T T T T F F F) = BYTE T T T F F F F T) /\
  (InvSbox (BYTE T T T T T F F T) = BYTE F T T F T F F T) /\
  (InvSbox (BYTE T T T T T F T F) = BYTE F F F T F T F F) /\
  (InvSbox (BYTE T T T T T F T T) = BYTE F T T F F F T T) /\
  (InvSbox (BYTE T T T T T T F F) = BYTE F T F T F T F T) /\
  (InvSbox (BYTE T T T T T T F T) = BYTE F F T F F F F T) /\
  (InvSbox (BYTE T T T T T T T F) = BYTE F F F F T T F F) /\
  (InvSbox (BYTE T T T T T T T T) = BYTE F T T T T T F T)`;

val GF256_by_2_def = Count.apply Define
 `(GF256_by_2 (BYTE F F F F F F F F) = BYTE F F F F F F F F) /\
  (GF256_by_2 (BYTE F F F F F F F T) = BYTE F F F F F F T F) /\
  (GF256_by_2 (BYTE F F F F F F T F) = BYTE F F F F F T F F) /\
  (GF256_by_2 (BYTE F F F F F F T T) = BYTE F F F F F T T F) /\
  (GF256_by_2 (BYTE F F F F F T F F) = BYTE F F F F T F F F) /\
  (GF256_by_2 (BYTE F F F F F T F T) = BYTE F F F F T F T F) /\
  (GF256_by_2 (BYTE F F F F F T T F) = BYTE F F F F T T F F) /\
  (GF256_by_2 (BYTE F F F F F T T T) = BYTE F F F F T T T F) /\
  (GF256_by_2 (BYTE F F F F T F F F) = BYTE F F F T F F F F) /\
  (GF256_by_2 (BYTE F F F F T F F T) = BYTE F F F T F F T F) /\
  (GF256_by_2 (BYTE F F F F T F T F) = BYTE F F F T F T F F) /\
  (GF256_by_2 (BYTE F F F F T F T T) = BYTE F F F T F T T F) /\
  (GF256_by_2 (BYTE F F F F T T F F) = BYTE F F F T T F F F) /\
  (GF256_by_2 (BYTE F F F F T T F T) = BYTE F F F T T F T F) /\
  (GF256_by_2 (BYTE F F F F T T T F) = BYTE F F F T T T F F) /\
  (GF256_by_2 (BYTE F F F F T T T T) = BYTE F F F T T T T F) /\
  (GF256_by_2 (BYTE F F F T F F F F) = BYTE F F T F F F F F) /\
  (GF256_by_2 (BYTE F F F T F F F T) = BYTE F F T F F F T F) /\
  (GF256_by_2 (BYTE F F F T F F T F) = BYTE F F T F F T F F) /\
  (GF256_by_2 (BYTE F F F T F F T T) = BYTE F F T F F T T F) /\
  (GF256_by_2 (BYTE F F F T F T F F) = BYTE F F T F T F F F) /\
  (GF256_by_2 (BYTE F F F T F T F T) = BYTE F F T F T F T F) /\
  (GF256_by_2 (BYTE F F F T F T T F) = BYTE F F T F T T F F) /\
  (GF256_by_2 (BYTE F F F T F T T T) = BYTE F F T F T T T F) /\
  (GF256_by_2 (BYTE F F F T T F F F) = BYTE F F T T F F F F) /\
  (GF256_by_2 (BYTE F F F T T F F T) = BYTE F F T T F F T F) /\
  (GF256_by_2 (BYTE F F F T T F T F) = BYTE F F T T F T F F) /\
  (GF256_by_2 (BYTE F F F T T F T T) = BYTE F F T T F T T F) /\
  (GF256_by_2 (BYTE F F F T T T F F) = BYTE F F T T T F F F) /\
  (GF256_by_2 (BYTE F F F T T T F T) = BYTE F F T T T F T F) /\
  (GF256_by_2 (BYTE F F F T T T T F) = BYTE F F T T T T F F) /\
  (GF256_by_2 (BYTE F F F T T T T T) = BYTE F F T T T T T F) /\
  (GF256_by_2 (BYTE F F T F F F F F) = BYTE F T F F F F F F) /\
  (GF256_by_2 (BYTE F F T F F F F T) = BYTE F T F F F F T F) /\
  (GF256_by_2 (BYTE F F T F F F T F) = BYTE F T F F F T F F) /\
  (GF256_by_2 (BYTE F F T F F F T T) = BYTE F T F F F T T F) /\
  (GF256_by_2 (BYTE F F T F F T F F) = BYTE F T F F T F F F) /\
  (GF256_by_2 (BYTE F F T F F T F T) = BYTE F T F F T F T F) /\
  (GF256_by_2 (BYTE F F T F F T T F) = BYTE F T F F T T F F) /\
  (GF256_by_2 (BYTE F F T F F T T T) = BYTE F T F F T T T F) /\
  (GF256_by_2 (BYTE F F T F T F F F) = BYTE F T F T F F F F) /\
  (GF256_by_2 (BYTE F F T F T F F T) = BYTE F T F T F F T F) /\
  (GF256_by_2 (BYTE F F T F T F T F) = BYTE F T F T F T F F) /\
  (GF256_by_2 (BYTE F F T F T F T T) = BYTE F T F T F T T F) /\
  (GF256_by_2 (BYTE F F T F T T F F) = BYTE F T F T T F F F) /\
  (GF256_by_2 (BYTE F F T F T T F T) = BYTE F T F T T F T F) /\
  (GF256_by_2 (BYTE F F T F T T T F) = BYTE F T F T T T F F) /\
  (GF256_by_2 (BYTE F F T F T T T T) = BYTE F T F T T T T F) /\
  (GF256_by_2 (BYTE F F T T F F F F) = BYTE F T T F F F F F) /\
  (GF256_by_2 (BYTE F F T T F F F T) = BYTE F T T F F F T F) /\
  (GF256_by_2 (BYTE F F T T F F T F) = BYTE F T T F F T F F) /\
  (GF256_by_2 (BYTE F F T T F F T T) = BYTE F T T F F T T F) /\
  (GF256_by_2 (BYTE F F T T F T F F) = BYTE F T T F T F F F) /\
  (GF256_by_2 (BYTE F F T T F T F T) = BYTE F T T F T F T F) /\
  (GF256_by_2 (BYTE F F T T F T T F) = BYTE F T T F T T F F) /\
  (GF256_by_2 (BYTE F F T T F T T T) = BYTE F T T F T T T F) /\
  (GF256_by_2 (BYTE F F T T T F F F) = BYTE F T T T F F F F) /\
  (GF256_by_2 (BYTE F F T T T F F T) = BYTE F T T T F F T F) /\
  (GF256_by_2 (BYTE F F T T T F T F) = BYTE F T T T F T F F) /\
  (GF256_by_2 (BYTE F F T T T F T T) = BYTE F T T T F T T F) /\
  (GF256_by_2 (BYTE F F T T T T F F) = BYTE F T T T T F F F) /\
  (GF256_by_2 (BYTE F F T T T T F T) = BYTE F T T T T F T F) /\
  (GF256_by_2 (BYTE F F T T T T T F) = BYTE F T T T T T F F) /\
  (GF256_by_2 (BYTE F F T T T T T T) = BYTE F T T T T T T F) /\
  (GF256_by_2 (BYTE F T F F F F F F) = BYTE T F F F F F F F) /\
  (GF256_by_2 (BYTE F T F F F F F T) = BYTE T F F F F F T F) /\
  (GF256_by_2 (BYTE F T F F F F T F) = BYTE T F F F F T F F) /\
  (GF256_by_2 (BYTE F T F F F F T T) = BYTE T F F F F T T F) /\
  (GF256_by_2 (BYTE F T F F F T F F) = BYTE T F F F T F F F) /\
  (GF256_by_2 (BYTE F T F F F T F T) = BYTE T F F F T F T F) /\
  (GF256_by_2 (BYTE F T F F F T T F) = BYTE T F F F T T F F) /\
  (GF256_by_2 (BYTE F T F F F T T T) = BYTE T F F F T T T F) /\
  (GF256_by_2 (BYTE F T F F T F F F) = BYTE T F F T F F F F) /\
  (GF256_by_2 (BYTE F T F F T F F T) = BYTE T F F T F F T F) /\
  (GF256_by_2 (BYTE F T F F T F T F) = BYTE T F F T F T F F) /\
  (GF256_by_2 (BYTE F T F F T F T T) = BYTE T F F T F T T F) /\
  (GF256_by_2 (BYTE F T F F T T F F) = BYTE T F F T T F F F) /\
  (GF256_by_2 (BYTE F T F F T T F T) = BYTE T F F T T F T F) /\
  (GF256_by_2 (BYTE F T F F T T T F) = BYTE T F F T T T F F) /\
  (GF256_by_2 (BYTE F T F F T T T T) = BYTE T F F T T T T F) /\
  (GF256_by_2 (BYTE F T F T F F F F) = BYTE T F T F F F F F) /\
  (GF256_by_2 (BYTE F T F T F F F T) = BYTE T F T F F F T F) /\
  (GF256_by_2 (BYTE F T F T F F T F) = BYTE T F T F F T F F) /\
  (GF256_by_2 (BYTE F T F T F F T T) = BYTE T F T F F T T F) /\
  (GF256_by_2 (BYTE F T F T F T F F) = BYTE T F T F T F F F) /\
  (GF256_by_2 (BYTE F T F T F T F T) = BYTE T F T F T F T F) /\
  (GF256_by_2 (BYTE F T F T F T T F) = BYTE T F T F T T F F) /\
  (GF256_by_2 (BYTE F T F T F T T T) = BYTE T F T F T T T F) /\
  (GF256_by_2 (BYTE F T F T T F F F) = BYTE T F T T F F F F) /\
  (GF256_by_2 (BYTE F T F T T F F T) = BYTE T F T T F F T F) /\
  (GF256_by_2 (BYTE F T F T T F T F) = BYTE T F T T F T F F) /\
  (GF256_by_2 (BYTE F T F T T F T T) = BYTE T F T T F T T F) /\
  (GF256_by_2 (BYTE F T F T T T F F) = BYTE T F T T T F F F) /\
  (GF256_by_2 (BYTE F T F T T T F T) = BYTE T F T T T F T F) /\
  (GF256_by_2 (BYTE F T F T T T T F) = BYTE T F T T T T F F) /\
  (GF256_by_2 (BYTE F T F T T T T T) = BYTE T F T T T T T F) /\
  (GF256_by_2 (BYTE F T T F F F F F) = BYTE T T F F F F F F) /\
  (GF256_by_2 (BYTE F T T F F F F T) = BYTE T T F F F F T F) /\
  (GF256_by_2 (BYTE F T T F F F T F) = BYTE T T F F F T F F) /\
  (GF256_by_2 (BYTE F T T F F F T T) = BYTE T T F F F T T F) /\
  (GF256_by_2 (BYTE F T T F F T F F) = BYTE T T F F T F F F) /\
  (GF256_by_2 (BYTE F T T F F T F T) = BYTE T T F F T F T F) /\
  (GF256_by_2 (BYTE F T T F F T T F) = BYTE T T F F T T F F) /\
  (GF256_by_2 (BYTE F T T F F T T T) = BYTE T T F F T T T F) /\
  (GF256_by_2 (BYTE F T T F T F F F) = BYTE T T F T F F F F) /\
  (GF256_by_2 (BYTE F T T F T F F T) = BYTE T T F T F F T F) /\
  (GF256_by_2 (BYTE F T T F T F T F) = BYTE T T F T F T F F) /\
  (GF256_by_2 (BYTE F T T F T F T T) = BYTE T T F T F T T F) /\
  (GF256_by_2 (BYTE F T T F T T F F) = BYTE T T F T T F F F) /\
  (GF256_by_2 (BYTE F T T F T T F T) = BYTE T T F T T F T F) /\
  (GF256_by_2 (BYTE F T T F T T T F) = BYTE T T F T T T F F) /\
  (GF256_by_2 (BYTE F T T F T T T T) = BYTE T T F T T T T F) /\
  (GF256_by_2 (BYTE F T T T F F F F) = BYTE T T T F F F F F) /\
  (GF256_by_2 (BYTE F T T T F F F T) = BYTE T T T F F F T F) /\
  (GF256_by_2 (BYTE F T T T F F T F) = BYTE T T T F F T F F) /\
  (GF256_by_2 (BYTE F T T T F F T T) = BYTE T T T F F T T F) /\
  (GF256_by_2 (BYTE F T T T F T F F) = BYTE T T T F T F F F) /\
  (GF256_by_2 (BYTE F T T T F T F T) = BYTE T T T F T F T F) /\
  (GF256_by_2 (BYTE F T T T F T T F) = BYTE T T T F T T F F) /\
  (GF256_by_2 (BYTE F T T T F T T T) = BYTE T T T F T T T F) /\
  (GF256_by_2 (BYTE F T T T T F F F) = BYTE T T T T F F F F) /\
  (GF256_by_2 (BYTE F T T T T F F T) = BYTE T T T T F F T F) /\
  (GF256_by_2 (BYTE F T T T T F T F) = BYTE T T T T F T F F) /\
  (GF256_by_2 (BYTE F T T T T F T T) = BYTE T T T T F T T F) /\
  (GF256_by_2 (BYTE F T T T T T F F) = BYTE T T T T T F F F) /\
  (GF256_by_2 (BYTE F T T T T T F T) = BYTE T T T T T F T F) /\
  (GF256_by_2 (BYTE F T T T T T T F) = BYTE T T T T T T F F) /\
  (GF256_by_2 (BYTE F T T T T T T T) = BYTE T T T T T T T F) /\
  (GF256_by_2 (BYTE T F F F F F F F) = BYTE F F F T T F T T) /\
  (GF256_by_2 (BYTE T F F F F F F T) = BYTE F F F T T F F T) /\
  (GF256_by_2 (BYTE T F F F F F T F) = BYTE F F F T T T T T) /\
  (GF256_by_2 (BYTE T F F F F F T T) = BYTE F F F T T T F T) /\
  (GF256_by_2 (BYTE T F F F F T F F) = BYTE F F F T F F T T) /\
  (GF256_by_2 (BYTE T F F F F T F T) = BYTE F F F T F F F T) /\
  (GF256_by_2 (BYTE T F F F F T T F) = BYTE F F F T F T T T) /\
  (GF256_by_2 (BYTE T F F F F T T T) = BYTE F F F T F T F T) /\
  (GF256_by_2 (BYTE T F F F T F F F) = BYTE F F F F T F T T) /\
  (GF256_by_2 (BYTE T F F F T F F T) = BYTE F F F F T F F T) /\
  (GF256_by_2 (BYTE T F F F T F T F) = BYTE F F F F T T T T) /\
  (GF256_by_2 (BYTE T F F F T F T T) = BYTE F F F F T T F T) /\
  (GF256_by_2 (BYTE T F F F T T F F) = BYTE F F F F F F T T) /\
  (GF256_by_2 (BYTE T F F F T T F T) = BYTE F F F F F F F T) /\
  (GF256_by_2 (BYTE T F F F T T T F) = BYTE F F F F F T T T) /\
  (GF256_by_2 (BYTE T F F F T T T T) = BYTE F F F F F T F T) /\
  (GF256_by_2 (BYTE T F F T F F F F) = BYTE F F T T T F T T) /\
  (GF256_by_2 (BYTE T F F T F F F T) = BYTE F F T T T F F T) /\
  (GF256_by_2 (BYTE T F F T F F T F) = BYTE F F T T T T T T) /\
  (GF256_by_2 (BYTE T F F T F F T T) = BYTE F F T T T T F T) /\
  (GF256_by_2 (BYTE T F F T F T F F) = BYTE F F T T F F T T) /\
  (GF256_by_2 (BYTE T F F T F T F T) = BYTE F F T T F F F T) /\
  (GF256_by_2 (BYTE T F F T F T T F) = BYTE F F T T F T T T) /\
  (GF256_by_2 (BYTE T F F T F T T T) = BYTE F F T T F T F T) /\
  (GF256_by_2 (BYTE T F F T T F F F) = BYTE F F T F T F T T) /\
  (GF256_by_2 (BYTE T F F T T F F T) = BYTE F F T F T F F T) /\
  (GF256_by_2 (BYTE T F F T T F T F) = BYTE F F T F T T T T) /\
  (GF256_by_2 (BYTE T F F T T F T T) = BYTE F F T F T T F T) /\
  (GF256_by_2 (BYTE T F F T T T F F) = BYTE F F T F F F T T) /\
  (GF256_by_2 (BYTE T F F T T T F T) = BYTE F F T F F F F T) /\
  (GF256_by_2 (BYTE T F F T T T T F) = BYTE F F T F F T T T) /\
  (GF256_by_2 (BYTE T F F T T T T T) = BYTE F F T F F T F T) /\
  (GF256_by_2 (BYTE T F T F F F F F) = BYTE F T F T T F T T) /\
  (GF256_by_2 (BYTE T F T F F F F T) = BYTE F T F T T F F T) /\
  (GF256_by_2 (BYTE T F T F F F T F) = BYTE F T F T T T T T) /\
  (GF256_by_2 (BYTE T F T F F F T T) = BYTE F T F T T T F T) /\
  (GF256_by_2 (BYTE T F T F F T F F) = BYTE F T F T F F T T) /\
  (GF256_by_2 (BYTE T F T F F T F T) = BYTE F T F T F F F T) /\
  (GF256_by_2 (BYTE T F T F F T T F) = BYTE F T F T F T T T) /\
  (GF256_by_2 (BYTE T F T F F T T T) = BYTE F T F T F T F T) /\
  (GF256_by_2 (BYTE T F T F T F F F) = BYTE F T F F T F T T) /\
  (GF256_by_2 (BYTE T F T F T F F T) = BYTE F T F F T F F T) /\
  (GF256_by_2 (BYTE T F T F T F T F) = BYTE F T F F T T T T) /\
  (GF256_by_2 (BYTE T F T F T F T T) = BYTE F T F F T T F T) /\
  (GF256_by_2 (BYTE T F T F T T F F) = BYTE F T F F F F T T) /\
  (GF256_by_2 (BYTE T F T F T T F T) = BYTE F T F F F F F T) /\
  (GF256_by_2 (BYTE T F T F T T T F) = BYTE F T F F F T T T) /\
  (GF256_by_2 (BYTE T F T F T T T T) = BYTE F T F F F T F T) /\
  (GF256_by_2 (BYTE T F T T F F F F) = BYTE F T T T T F T T) /\
  (GF256_by_2 (BYTE T F T T F F F T) = BYTE F T T T T F F T) /\
  (GF256_by_2 (BYTE T F T T F F T F) = BYTE F T T T T T T T) /\
  (GF256_by_2 (BYTE T F T T F F T T) = BYTE F T T T T T F T) /\
  (GF256_by_2 (BYTE T F T T F T F F) = BYTE F T T T F F T T) /\
  (GF256_by_2 (BYTE T F T T F T F T) = BYTE F T T T F F F T) /\
  (GF256_by_2 (BYTE T F T T F T T F) = BYTE F T T T F T T T) /\
  (GF256_by_2 (BYTE T F T T F T T T) = BYTE F T T T F T F T) /\
  (GF256_by_2 (BYTE T F T T T F F F) = BYTE F T T F T F T T) /\
  (GF256_by_2 (BYTE T F T T T F F T) = BYTE F T T F T F F T) /\
  (GF256_by_2 (BYTE T F T T T F T F) = BYTE F T T F T T T T) /\
  (GF256_by_2 (BYTE T F T T T F T T) = BYTE F T T F T T F T) /\
  (GF256_by_2 (BYTE T F T T T T F F) = BYTE F T T F F F T T) /\
  (GF256_by_2 (BYTE T F T T T T F T) = BYTE F T T F F F F T) /\
  (GF256_by_2 (BYTE T F T T T T T F) = BYTE F T T F F T T T) /\
  (GF256_by_2 (BYTE T F T T T T T T) = BYTE F T T F F T F T) /\
  (GF256_by_2 (BYTE T T F F F F F F) = BYTE T F F T T F T T) /\
  (GF256_by_2 (BYTE T T F F F F F T) = BYTE T F F T T F F T) /\
  (GF256_by_2 (BYTE T T F F F F T F) = BYTE T F F T T T T T) /\
  (GF256_by_2 (BYTE T T F F F F T T) = BYTE T F F T T T F T) /\
  (GF256_by_2 (BYTE T T F F F T F F) = BYTE T F F T F F T T) /\
  (GF256_by_2 (BYTE T T F F F T F T) = BYTE T F F T F F F T) /\
  (GF256_by_2 (BYTE T T F F F T T F) = BYTE T F F T F T T T) /\
  (GF256_by_2 (BYTE T T F F F T T T) = BYTE T F F T F T F T) /\
  (GF256_by_2 (BYTE T T F F T F F F) = BYTE T F F F T F T T) /\
  (GF256_by_2 (BYTE T T F F T F F T) = BYTE T F F F T F F T) /\
  (GF256_by_2 (BYTE T T F F T F T F) = BYTE T F F F T T T T) /\
  (GF256_by_2 (BYTE T T F F T F T T) = BYTE T F F F T T F T) /\
  (GF256_by_2 (BYTE T T F F T T F F) = BYTE T F F F F F T T) /\
  (GF256_by_2 (BYTE T T F F T T F T) = BYTE T F F F F F F T) /\
  (GF256_by_2 (BYTE T T F F T T T F) = BYTE T F F F F T T T) /\
  (GF256_by_2 (BYTE T T F F T T T T) = BYTE T F F F F T F T) /\
  (GF256_by_2 (BYTE T T F T F F F F) = BYTE T F T T T F T T) /\
  (GF256_by_2 (BYTE T T F T F F F T) = BYTE T F T T T F F T) /\
  (GF256_by_2 (BYTE T T F T F F T F) = BYTE T F T T T T T T) /\
  (GF256_by_2 (BYTE T T F T F F T T) = BYTE T F T T T T F T) /\
  (GF256_by_2 (BYTE T T F T F T F F) = BYTE T F T T F F T T) /\
  (GF256_by_2 (BYTE T T F T F T F T) = BYTE T F T T F F F T) /\
  (GF256_by_2 (BYTE T T F T F T T F) = BYTE T F T T F T T T) /\
  (GF256_by_2 (BYTE T T F T F T T T) = BYTE T F T T F T F T) /\
  (GF256_by_2 (BYTE T T F T T F F F) = BYTE T F T F T F T T) /\
  (GF256_by_2 (BYTE T T F T T F F T) = BYTE T F T F T F F T) /\
  (GF256_by_2 (BYTE T T F T T F T F) = BYTE T F T F T T T T) /\
  (GF256_by_2 (BYTE T T F T T F T T) = BYTE T F T F T T F T) /\
  (GF256_by_2 (BYTE T T F T T T F F) = BYTE T F T F F F T T) /\
  (GF256_by_2 (BYTE T T F T T T F T) = BYTE T F T F F F F T) /\
  (GF256_by_2 (BYTE T T F T T T T F) = BYTE T F T F F T T T) /\
  (GF256_by_2 (BYTE T T F T T T T T) = BYTE T F T F F T F T) /\
  (GF256_by_2 (BYTE T T T F F F F F) = BYTE T T F T T F T T) /\
  (GF256_by_2 (BYTE T T T F F F F T) = BYTE T T F T T F F T) /\
  (GF256_by_2 (BYTE T T T F F F T F) = BYTE T T F T T T T T) /\
  (GF256_by_2 (BYTE T T T F F F T T) = BYTE T T F T T T F T) /\
  (GF256_by_2 (BYTE T T T F F T F F) = BYTE T T F T F F T T) /\
  (GF256_by_2 (BYTE T T T F F T F T) = BYTE T T F T F F F T) /\
  (GF256_by_2 (BYTE T T T F F T T F) = BYTE T T F T F T T T) /\
  (GF256_by_2 (BYTE T T T F F T T T) = BYTE T T F T F T F T) /\
  (GF256_by_2 (BYTE T T T F T F F F) = BYTE T T F F T F T T) /\
  (GF256_by_2 (BYTE T T T F T F F T) = BYTE T T F F T F F T) /\
  (GF256_by_2 (BYTE T T T F T F T F) = BYTE T T F F T T T T) /\
  (GF256_by_2 (BYTE T T T F T F T T) = BYTE T T F F T T F T) /\
  (GF256_by_2 (BYTE T T T F T T F F) = BYTE T T F F F F T T) /\
  (GF256_by_2 (BYTE T T T F T T F T) = BYTE T T F F F F F T) /\
  (GF256_by_2 (BYTE T T T F T T T F) = BYTE T T F F F T T T) /\
  (GF256_by_2 (BYTE T T T F T T T T) = BYTE T T F F F T F T) /\
  (GF256_by_2 (BYTE T T T T F F F F) = BYTE T T T T T F T T) /\
  (GF256_by_2 (BYTE T T T T F F F T) = BYTE T T T T T F F T) /\
  (GF256_by_2 (BYTE T T T T F F T F) = BYTE T T T T T T T T) /\
  (GF256_by_2 (BYTE T T T T F F T T) = BYTE T T T T T T F T) /\
  (GF256_by_2 (BYTE T T T T F T F F) = BYTE T T T T F F T T) /\
  (GF256_by_2 (BYTE T T T T F T F T) = BYTE T T T T F F F T) /\
  (GF256_by_2 (BYTE T T T T F T T F) = BYTE T T T T F T T T) /\
  (GF256_by_2 (BYTE T T T T F T T T) = BYTE T T T T F T F T) /\
  (GF256_by_2 (BYTE T T T T T F F F) = BYTE T T T F T F T T) /\
  (GF256_by_2 (BYTE T T T T T F F T) = BYTE T T T F T F F T) /\
  (GF256_by_2 (BYTE T T T T T F T F) = BYTE T T T F T T T T) /\
  (GF256_by_2 (BYTE T T T T T F T T) = BYTE T T T F T T F T) /\
  (GF256_by_2 (BYTE T T T T T T F F) = BYTE T T T F F F T T) /\
  (GF256_by_2 (BYTE T T T T T T F T) = BYTE T T T F F F F T) /\
  (GF256_by_2 (BYTE T T T T T T T F) = BYTE T T T F F T T T) /\
  (GF256_by_2 (BYTE T T T T T T T T) = BYTE T T T F F T F T)`;

val GF256_by_3_def = Count.apply Define
 `(GF256_by_3 (BYTE F F F F F F F F) = BYTE F F F F F F F F) /\
  (GF256_by_3 (BYTE F F F F F F F T) = BYTE F F F F F F T T) /\
  (GF256_by_3 (BYTE F F F F F F T F) = BYTE F F F F F T T F) /\
  (GF256_by_3 (BYTE F F F F F F T T) = BYTE F F F F F T F T) /\
  (GF256_by_3 (BYTE F F F F F T F F) = BYTE F F F F T T F F) /\
  (GF256_by_3 (BYTE F F F F F T F T) = BYTE F F F F T T T T) /\
  (GF256_by_3 (BYTE F F F F F T T F) = BYTE F F F F T F T F) /\
  (GF256_by_3 (BYTE F F F F F T T T) = BYTE F F F F T F F T) /\
  (GF256_by_3 (BYTE F F F F T F F F) = BYTE F F F T T F F F) /\
  (GF256_by_3 (BYTE F F F F T F F T) = BYTE F F F T T F T T) /\
  (GF256_by_3 (BYTE F F F F T F T F) = BYTE F F F T T T T F) /\
  (GF256_by_3 (BYTE F F F F T F T T) = BYTE F F F T T T F T) /\
  (GF256_by_3 (BYTE F F F F T T F F) = BYTE F F F T F T F F) /\
  (GF256_by_3 (BYTE F F F F T T F T) = BYTE F F F T F T T T) /\
  (GF256_by_3 (BYTE F F F F T T T F) = BYTE F F F T F F T F) /\
  (GF256_by_3 (BYTE F F F F T T T T) = BYTE F F F T F F F T) /\
  (GF256_by_3 (BYTE F F F T F F F F) = BYTE F F T T F F F F) /\
  (GF256_by_3 (BYTE F F F T F F F T) = BYTE F F T T F F T T) /\
  (GF256_by_3 (BYTE F F F T F F T F) = BYTE F F T T F T T F) /\
  (GF256_by_3 (BYTE F F F T F F T T) = BYTE F F T T F T F T) /\
  (GF256_by_3 (BYTE F F F T F T F F) = BYTE F F T T T T F F) /\
  (GF256_by_3 (BYTE F F F T F T F T) = BYTE F F T T T T T T) /\
  (GF256_by_3 (BYTE F F F T F T T F) = BYTE F F T T T F T F) /\
  (GF256_by_3 (BYTE F F F T F T T T) = BYTE F F T T T F F T) /\
  (GF256_by_3 (BYTE F F F T T F F F) = BYTE F F T F T F F F) /\
  (GF256_by_3 (BYTE F F F T T F F T) = BYTE F F T F T F T T) /\
  (GF256_by_3 (BYTE F F F T T F T F) = BYTE F F T F T T T F) /\
  (GF256_by_3 (BYTE F F F T T F T T) = BYTE F F T F T T F T) /\
  (GF256_by_3 (BYTE F F F T T T F F) = BYTE F F T F F T F F) /\
  (GF256_by_3 (BYTE F F F T T T F T) = BYTE F F T F F T T T) /\
  (GF256_by_3 (BYTE F F F T T T T F) = BYTE F F T F F F T F) /\
  (GF256_by_3 (BYTE F F F T T T T T) = BYTE F F T F F F F T) /\
  (GF256_by_3 (BYTE F F T F F F F F) = BYTE F T T F F F F F) /\
  (GF256_by_3 (BYTE F F T F F F F T) = BYTE F T T F F F T T) /\
  (GF256_by_3 (BYTE F F T F F F T F) = BYTE F T T F F T T F) /\
  (GF256_by_3 (BYTE F F T F F F T T) = BYTE F T T F F T F T) /\
  (GF256_by_3 (BYTE F F T F F T F F) = BYTE F T T F T T F F) /\
  (GF256_by_3 (BYTE F F T F F T F T) = BYTE F T T F T T T T) /\
  (GF256_by_3 (BYTE F F T F F T T F) = BYTE F T T F T F T F) /\
  (GF256_by_3 (BYTE F F T F F T T T) = BYTE F T T F T F F T) /\
  (GF256_by_3 (BYTE F F T F T F F F) = BYTE F T T T T F F F) /\
  (GF256_by_3 (BYTE F F T F T F F T) = BYTE F T T T T F T T) /\
  (GF256_by_3 (BYTE F F T F T F T F) = BYTE F T T T T T T F) /\
  (GF256_by_3 (BYTE F F T F T F T T) = BYTE F T T T T T F T) /\
  (GF256_by_3 (BYTE F F T F T T F F) = BYTE F T T T F T F F) /\
  (GF256_by_3 (BYTE F F T F T T F T) = BYTE F T T T F T T T) /\
  (GF256_by_3 (BYTE F F T F T T T F) = BYTE F T T T F F T F) /\
  (GF256_by_3 (BYTE F F T F T T T T) = BYTE F T T T F F F T) /\
  (GF256_by_3 (BYTE F F T T F F F F) = BYTE F T F T F F F F) /\
  (GF256_by_3 (BYTE F F T T F F F T) = BYTE F T F T F F T T) /\
  (GF256_by_3 (BYTE F F T T F F T F) = BYTE F T F T F T T F) /\
  (GF256_by_3 (BYTE F F T T F F T T) = BYTE F T F T F T F T) /\
  (GF256_by_3 (BYTE F F T T F T F F) = BYTE F T F T T T F F) /\
  (GF256_by_3 (BYTE F F T T F T F T) = BYTE F T F T T T T T) /\
  (GF256_by_3 (BYTE F F T T F T T F) = BYTE F T F T T F T F) /\
  (GF256_by_3 (BYTE F F T T F T T T) = BYTE F T F T T F F T) /\
  (GF256_by_3 (BYTE F F T T T F F F) = BYTE F T F F T F F F) /\
  (GF256_by_3 (BYTE F F T T T F F T) = BYTE F T F F T F T T) /\
  (GF256_by_3 (BYTE F F T T T F T F) = BYTE F T F F T T T F) /\
  (GF256_by_3 (BYTE F F T T T F T T) = BYTE F T F F T T F T) /\
  (GF256_by_3 (BYTE F F T T T T F F) = BYTE F T F F F T F F) /\
  (GF256_by_3 (BYTE F F T T T T F T) = BYTE F T F F F T T T) /\
  (GF256_by_3 (BYTE F F T T T T T F) = BYTE F T F F F F T F) /\
  (GF256_by_3 (BYTE F F T T T T T T) = BYTE F T F F F F F T) /\
  (GF256_by_3 (BYTE F T F F F F F F) = BYTE T T F F F F F F) /\
  (GF256_by_3 (BYTE F T F F F F F T) = BYTE T T F F F F T T) /\
  (GF256_by_3 (BYTE F T F F F F T F) = BYTE T T F F F T T F) /\
  (GF256_by_3 (BYTE F T F F F F T T) = BYTE T T F F F T F T) /\
  (GF256_by_3 (BYTE F T F F F T F F) = BYTE T T F F T T F F) /\
  (GF256_by_3 (BYTE F T F F F T F T) = BYTE T T F F T T T T) /\
  (GF256_by_3 (BYTE F T F F F T T F) = BYTE T T F F T F T F) /\
  (GF256_by_3 (BYTE F T F F F T T T) = BYTE T T F F T F F T) /\
  (GF256_by_3 (BYTE F T F F T F F F) = BYTE T T F T T F F F) /\
  (GF256_by_3 (BYTE F T F F T F F T) = BYTE T T F T T F T T) /\
  (GF256_by_3 (BYTE F T F F T F T F) = BYTE T T F T T T T F) /\
  (GF256_by_3 (BYTE F T F F T F T T) = BYTE T T F T T T F T) /\
  (GF256_by_3 (BYTE F T F F T T F F) = BYTE T T F T F T F F) /\
  (GF256_by_3 (BYTE F T F F T T F T) = BYTE T T F T F T T T) /\
  (GF256_by_3 (BYTE F T F F T T T F) = BYTE T T F T F F T F) /\
  (GF256_by_3 (BYTE F T F F T T T T) = BYTE T T F T F F F T) /\
  (GF256_by_3 (BYTE F T F T F F F F) = BYTE T T T T F F F F) /\
  (GF256_by_3 (BYTE F T F T F F F T) = BYTE T T T T F F T T) /\
  (GF256_by_3 (BYTE F T F T F F T F) = BYTE T T T T F T T F) /\
  (GF256_by_3 (BYTE F T F T F F T T) = BYTE T T T T F T F T) /\
  (GF256_by_3 (BYTE F T F T F T F F) = BYTE T T T T T T F F) /\
  (GF256_by_3 (BYTE F T F T F T F T) = BYTE T T T T T T T T) /\
  (GF256_by_3 (BYTE F T F T F T T F) = BYTE T T T T T F T F) /\
  (GF256_by_3 (BYTE F T F T F T T T) = BYTE T T T T T F F T) /\
  (GF256_by_3 (BYTE F T F T T F F F) = BYTE T T T F T F F F) /\
  (GF256_by_3 (BYTE F T F T T F F T) = BYTE T T T F T F T T) /\
  (GF256_by_3 (BYTE F T F T T F T F) = BYTE T T T F T T T F) /\
  (GF256_by_3 (BYTE F T F T T F T T) = BYTE T T T F T T F T) /\
  (GF256_by_3 (BYTE F T F T T T F F) = BYTE T T T F F T F F) /\
  (GF256_by_3 (BYTE F T F T T T F T) = BYTE T T T F F T T T) /\
  (GF256_by_3 (BYTE F T F T T T T F) = BYTE T T T F F F T F) /\
  (GF256_by_3 (BYTE F T F T T T T T) = BYTE T T T F F F F T) /\
  (GF256_by_3 (BYTE F T T F F F F F) = BYTE T F T F F F F F) /\
  (GF256_by_3 (BYTE F T T F F F F T) = BYTE T F T F F F T T) /\
  (GF256_by_3 (BYTE F T T F F F T F) = BYTE T F T F F T T F) /\
  (GF256_by_3 (BYTE F T T F F F T T) = BYTE T F T F F T F T) /\
  (GF256_by_3 (BYTE F T T F F T F F) = BYTE T F T F T T F F) /\
  (GF256_by_3 (BYTE F T T F F T F T) = BYTE T F T F T T T T) /\
  (GF256_by_3 (BYTE F T T F F T T F) = BYTE T F T F T F T F) /\
  (GF256_by_3 (BYTE F T T F F T T T) = BYTE T F T F T F F T) /\
  (GF256_by_3 (BYTE F T T F T F F F) = BYTE T F T T T F F F) /\
  (GF256_by_3 (BYTE F T T F T F F T) = BYTE T F T T T F T T) /\
  (GF256_by_3 (BYTE F T T F T F T F) = BYTE T F T T T T T F) /\
  (GF256_by_3 (BYTE F T T F T F T T) = BYTE T F T T T T F T) /\
  (GF256_by_3 (BYTE F T T F T T F F) = BYTE T F T T F T F F) /\
  (GF256_by_3 (BYTE F T T F T T F T) = BYTE T F T T F T T T) /\
  (GF256_by_3 (BYTE F T T F T T T F) = BYTE T F T T F F T F) /\
  (GF256_by_3 (BYTE F T T F T T T T) = BYTE T F T T F F F T) /\
  (GF256_by_3 (BYTE F T T T F F F F) = BYTE T F F T F F F F) /\
  (GF256_by_3 (BYTE F T T T F F F T) = BYTE T F F T F F T T) /\
  (GF256_by_3 (BYTE F T T T F F T F) = BYTE T F F T F T T F) /\
  (GF256_by_3 (BYTE F T T T F F T T) = BYTE T F F T F T F T) /\
  (GF256_by_3 (BYTE F T T T F T F F) = BYTE T F F T T T F F) /\
  (GF256_by_3 (BYTE F T T T F T F T) = BYTE T F F T T T T T) /\
  (GF256_by_3 (BYTE F T T T F T T F) = BYTE T F F T T F T F) /\
  (GF256_by_3 (BYTE F T T T F T T T) = BYTE T F F T T F F T) /\
  (GF256_by_3 (BYTE F T T T T F F F) = BYTE T F F F T F F F) /\
  (GF256_by_3 (BYTE F T T T T F F T) = BYTE T F F F T F T T) /\
  (GF256_by_3 (BYTE F T T T T F T F) = BYTE T F F F T T T F) /\
  (GF256_by_3 (BYTE F T T T T F T T) = BYTE T F F F T T F T) /\
  (GF256_by_3 (BYTE F T T T T T F F) = BYTE T F F F F T F F) /\
  (GF256_by_3 (BYTE F T T T T T F T) = BYTE T F F F F T T T) /\
  (GF256_by_3 (BYTE F T T T T T T F) = BYTE T F F F F F T F) /\
  (GF256_by_3 (BYTE F T T T T T T T) = BYTE T F F F F F F T) /\
  (GF256_by_3 (BYTE T F F F F F F F) = BYTE T F F T T F T T) /\
  (GF256_by_3 (BYTE T F F F F F F T) = BYTE T F F T T F F F) /\
  (GF256_by_3 (BYTE T F F F F F T F) = BYTE T F F T T T F T) /\
  (GF256_by_3 (BYTE T F F F F F T T) = BYTE T F F T T T T F) /\
  (GF256_by_3 (BYTE T F F F F T F F) = BYTE T F F T F T T T) /\
  (GF256_by_3 (BYTE T F F F F T F T) = BYTE T F F T F T F F) /\
  (GF256_by_3 (BYTE T F F F F T T F) = BYTE T F F T F F F T) /\
  (GF256_by_3 (BYTE T F F F F T T T) = BYTE T F F T F F T F) /\
  (GF256_by_3 (BYTE T F F F T F F F) = BYTE T F F F F F T T) /\
  (GF256_by_3 (BYTE T F F F T F F T) = BYTE T F F F F F F F) /\
  (GF256_by_3 (BYTE T F F F T F T F) = BYTE T F F F F T F T) /\
  (GF256_by_3 (BYTE T F F F T F T T) = BYTE T F F F F T T F) /\
  (GF256_by_3 (BYTE T F F F T T F F) = BYTE T F F F T T T T) /\
  (GF256_by_3 (BYTE T F F F T T F T) = BYTE T F F F T T F F) /\
  (GF256_by_3 (BYTE T F F F T T T F) = BYTE T F F F T F F T) /\
  (GF256_by_3 (BYTE T F F F T T T T) = BYTE T F F F T F T F) /\
  (GF256_by_3 (BYTE T F F T F F F F) = BYTE T F T F T F T T) /\
  (GF256_by_3 (BYTE T F F T F F F T) = BYTE T F T F T F F F) /\
  (GF256_by_3 (BYTE T F F T F F T F) = BYTE T F T F T T F T) /\
  (GF256_by_3 (BYTE T F F T F F T T) = BYTE T F T F T T T F) /\
  (GF256_by_3 (BYTE T F F T F T F F) = BYTE T F T F F T T T) /\
  (GF256_by_3 (BYTE T F F T F T F T) = BYTE T F T F F T F F) /\
  (GF256_by_3 (BYTE T F F T F T T F) = BYTE T F T F F F F T) /\
  (GF256_by_3 (BYTE T F F T F T T T) = BYTE T F T F F F T F) /\
  (GF256_by_3 (BYTE T F F T T F F F) = BYTE T F T T F F T T) /\
  (GF256_by_3 (BYTE T F F T T F F T) = BYTE T F T T F F F F) /\
  (GF256_by_3 (BYTE T F F T T F T F) = BYTE T F T T F T F T) /\
  (GF256_by_3 (BYTE T F F T T F T T) = BYTE T F T T F T T F) /\
  (GF256_by_3 (BYTE T F F T T T F F) = BYTE T F T T T T T T) /\
  (GF256_by_3 (BYTE T F F T T T F T) = BYTE T F T T T T F F) /\
  (GF256_by_3 (BYTE T F F T T T T F) = BYTE T F T T T F F T) /\
  (GF256_by_3 (BYTE T F F T T T T T) = BYTE T F T T T F T F) /\
  (GF256_by_3 (BYTE T F T F F F F F) = BYTE T T T T T F T T) /\
  (GF256_by_3 (BYTE T F T F F F F T) = BYTE T T T T T F F F) /\
  (GF256_by_3 (BYTE T F T F F F T F) = BYTE T T T T T T F T) /\
  (GF256_by_3 (BYTE T F T F F F T T) = BYTE T T T T T T T F) /\
  (GF256_by_3 (BYTE T F T F F T F F) = BYTE T T T T F T T T) /\
  (GF256_by_3 (BYTE T F T F F T F T) = BYTE T T T T F T F F) /\
  (GF256_by_3 (BYTE T F T F F T T F) = BYTE T T T T F F F T) /\
  (GF256_by_3 (BYTE T F T F F T T T) = BYTE T T T T F F T F) /\
  (GF256_by_3 (BYTE T F T F T F F F) = BYTE T T T F F F T T) /\
  (GF256_by_3 (BYTE T F T F T F F T) = BYTE T T T F F F F F) /\
  (GF256_by_3 (BYTE T F T F T F T F) = BYTE T T T F F T F T) /\
  (GF256_by_3 (BYTE T F T F T F T T) = BYTE T T T F F T T F) /\
  (GF256_by_3 (BYTE T F T F T T F F) = BYTE T T T F T T T T) /\
  (GF256_by_3 (BYTE T F T F T T F T) = BYTE T T T F T T F F) /\
  (GF256_by_3 (BYTE T F T F T T T F) = BYTE T T T F T F F T) /\
  (GF256_by_3 (BYTE T F T F T T T T) = BYTE T T T F T F T F) /\
  (GF256_by_3 (BYTE T F T T F F F F) = BYTE T T F F T F T T) /\
  (GF256_by_3 (BYTE T F T T F F F T) = BYTE T T F F T F F F) /\
  (GF256_by_3 (BYTE T F T T F F T F) = BYTE T T F F T T F T) /\
  (GF256_by_3 (BYTE T F T T F F T T) = BYTE T T F F T T T F) /\
  (GF256_by_3 (BYTE T F T T F T F F) = BYTE T T F F F T T T) /\
  (GF256_by_3 (BYTE T F T T F T F T) = BYTE T T F F F T F F) /\
  (GF256_by_3 (BYTE T F T T F T T F) = BYTE T T F F F F F T) /\
  (GF256_by_3 (BYTE T F T T F T T T) = BYTE T T F F F F T F) /\
  (GF256_by_3 (BYTE T F T T T F F F) = BYTE T T F T F F T T) /\
  (GF256_by_3 (BYTE T F T T T F F T) = BYTE T T F T F F F F) /\
  (GF256_by_3 (BYTE T F T T T F T F) = BYTE T T F T F T F T) /\
  (GF256_by_3 (BYTE T F T T T F T T) = BYTE T T F T F T T F) /\
  (GF256_by_3 (BYTE T F T T T T F F) = BYTE T T F T T T T T) /\
  (GF256_by_3 (BYTE T F T T T T F T) = BYTE T T F T T T F F) /\
  (GF256_by_3 (BYTE T F T T T T T F) = BYTE T T F T T F F T) /\
  (GF256_by_3 (BYTE T F T T T T T T) = BYTE T T F T T F T F) /\
  (GF256_by_3 (BYTE T T F F F F F F) = BYTE F T F T T F T T) /\
  (GF256_by_3 (BYTE T T F F F F F T) = BYTE F T F T T F F F) /\
  (GF256_by_3 (BYTE T T F F F F T F) = BYTE F T F T T T F T) /\
  (GF256_by_3 (BYTE T T F F F F T T) = BYTE F T F T T T T F) /\
  (GF256_by_3 (BYTE T T F F F T F F) = BYTE F T F T F T T T) /\
  (GF256_by_3 (BYTE T T F F F T F T) = BYTE F T F T F T F F) /\
  (GF256_by_3 (BYTE T T F F F T T F) = BYTE F T F T F F F T) /\
  (GF256_by_3 (BYTE T T F F F T T T) = BYTE F T F T F F T F) /\
  (GF256_by_3 (BYTE T T F F T F F F) = BYTE F T F F F F T T) /\
  (GF256_by_3 (BYTE T T F F T F F T) = BYTE F T F F F F F F) /\
  (GF256_by_3 (BYTE T T F F T F T F) = BYTE F T F F F T F T) /\
  (GF256_by_3 (BYTE T T F F T F T T) = BYTE F T F F F T T F) /\
  (GF256_by_3 (BYTE T T F F T T F F) = BYTE F T F F T T T T) /\
  (GF256_by_3 (BYTE T T F F T T F T) = BYTE F T F F T T F F) /\
  (GF256_by_3 (BYTE T T F F T T T F) = BYTE F T F F T F F T) /\
  (GF256_by_3 (BYTE T T F F T T T T) = BYTE F T F F T F T F) /\
  (GF256_by_3 (BYTE T T F T F F F F) = BYTE F T T F T F T T) /\
  (GF256_by_3 (BYTE T T F T F F F T) = BYTE F T T F T F F F) /\
  (GF256_by_3 (BYTE T T F T F F T F) = BYTE F T T F T T F T) /\
  (GF256_by_3 (BYTE T T F T F F T T) = BYTE F T T F T T T F) /\
  (GF256_by_3 (BYTE T T F T F T F F) = BYTE F T T F F T T T) /\
  (GF256_by_3 (BYTE T T F T F T F T) = BYTE F T T F F T F F) /\
  (GF256_by_3 (BYTE T T F T F T T F) = BYTE F T T F F F F T) /\
  (GF256_by_3 (BYTE T T F T F T T T) = BYTE F T T F F F T F) /\
  (GF256_by_3 (BYTE T T F T T F F F) = BYTE F T T T F F T T) /\
  (GF256_by_3 (BYTE T T F T T F F T) = BYTE F T T T F F F F) /\
  (GF256_by_3 (BYTE T T F T T F T F) = BYTE F T T T F T F T) /\
  (GF256_by_3 (BYTE T T F T T F T T) = BYTE F T T T F T T F) /\
  (GF256_by_3 (BYTE T T F T T T F F) = BYTE F T T T T T T T) /\
  (GF256_by_3 (BYTE T T F T T T F T) = BYTE F T T T T T F F) /\
  (GF256_by_3 (BYTE T T F T T T T F) = BYTE F T T T T F F T) /\
  (GF256_by_3 (BYTE T T F T T T T T) = BYTE F T T T T F T F) /\
  (GF256_by_3 (BYTE T T T F F F F F) = BYTE F F T T T F T T) /\
  (GF256_by_3 (BYTE T T T F F F F T) = BYTE F F T T T F F F) /\
  (GF256_by_3 (BYTE T T T F F F T F) = BYTE F F T T T T F T) /\
  (GF256_by_3 (BYTE T T T F F F T T) = BYTE F F T T T T T F) /\
  (GF256_by_3 (BYTE T T T F F T F F) = BYTE F F T T F T T T) /\
  (GF256_by_3 (BYTE T T T F F T F T) = BYTE F F T T F T F F) /\
  (GF256_by_3 (BYTE T T T F F T T F) = BYTE F F T T F F F T) /\
  (GF256_by_3 (BYTE T T T F F T T T) = BYTE F F T T F F T F) /\
  (GF256_by_3 (BYTE T T T F T F F F) = BYTE F F T F F F T T) /\
  (GF256_by_3 (BYTE T T T F T F F T) = BYTE F F T F F F F F) /\
  (GF256_by_3 (BYTE T T T F T F T F) = BYTE F F T F F T F T) /\
  (GF256_by_3 (BYTE T T T F T F T T) = BYTE F F T F F T T F) /\
  (GF256_by_3 (BYTE T T T F T T F F) = BYTE F F T F T T T T) /\
  (GF256_by_3 (BYTE T T T F T T F T) = BYTE F F T F T T F F) /\
  (GF256_by_3 (BYTE T T T F T T T F) = BYTE F F T F T F F T) /\
  (GF256_by_3 (BYTE T T T F T T T T) = BYTE F F T F T F T F) /\
  (GF256_by_3 (BYTE T T T T F F F F) = BYTE F F F F T F T T) /\
  (GF256_by_3 (BYTE T T T T F F F T) = BYTE F F F F T F F F) /\
  (GF256_by_3 (BYTE T T T T F F T F) = BYTE F F F F T T F T) /\
  (GF256_by_3 (BYTE T T T T F F T T) = BYTE F F F F T T T F) /\
  (GF256_by_3 (BYTE T T T T F T F F) = BYTE F F F F F T T T) /\
  (GF256_by_3 (BYTE T T T T F T F T) = BYTE F F F F F T F F) /\
  (GF256_by_3 (BYTE T T T T F T T F) = BYTE F F F F F F F T) /\
  (GF256_by_3 (BYTE T T T T F T T T) = BYTE F F F F F F T F) /\
  (GF256_by_3 (BYTE T T T T T F F F) = BYTE F F F T F F T T) /\
  (GF256_by_3 (BYTE T T T T T F F T) = BYTE F F F T F F F F) /\
  (GF256_by_3 (BYTE T T T T T F T F) = BYTE F F F T F T F T) /\
  (GF256_by_3 (BYTE T T T T T F T T) = BYTE F F F T F T T F) /\
  (GF256_by_3 (BYTE T T T T T T F F) = BYTE F F F T T T T T) /\
  (GF256_by_3 (BYTE T T T T T T F T) = BYTE F F F T T T F F) /\
  (GF256_by_3 (BYTE T T T T T T T F) = BYTE F F F T T F F T) /\
  (GF256_by_3 (BYTE T T T T T T T T) = BYTE F F F T T F T F)`;

val GF256_by_9_def_def = Count.apply Define
 `(GF256_by_9 (BYTE F F F F F F F F) = BYTE F F F F F F F F) /\
  (GF256_by_9 (BYTE F F F F F F F T) = BYTE F F F F T F F T) /\
  (GF256_by_9 (BYTE F F F F F F T F) = BYTE F F F T F F T F) /\
  (GF256_by_9 (BYTE F F F F F F T T) = BYTE F F F T T F T T) /\
  (GF256_by_9 (BYTE F F F F F T F F) = BYTE F F T F F T F F) /\
  (GF256_by_9 (BYTE F F F F F T F T) = BYTE F F T F T T F T) /\
  (GF256_by_9 (BYTE F F F F F T T F) = BYTE F F T T F T T F) /\
  (GF256_by_9 (BYTE F F F F F T T T) = BYTE F F T T T T T T) /\
  (GF256_by_9 (BYTE F F F F T F F F) = BYTE F T F F T F F F) /\
  (GF256_by_9 (BYTE F F F F T F F T) = BYTE F T F F F F F T) /\
  (GF256_by_9 (BYTE F F F F T F T F) = BYTE F T F T T F T F) /\
  (GF256_by_9 (BYTE F F F F T F T T) = BYTE F T F T F F T T) /\
  (GF256_by_9 (BYTE F F F F T T F F) = BYTE F T T F T T F F) /\
  (GF256_by_9 (BYTE F F F F T T F T) = BYTE F T T F F T F T) /\
  (GF256_by_9 (BYTE F F F F T T T F) = BYTE F T T T T T T F) /\
  (GF256_by_9 (BYTE F F F F T T T T) = BYTE F T T T F T T T) /\
  (GF256_by_9 (BYTE F F F T F F F F) = BYTE T F F T F F F F) /\
  (GF256_by_9 (BYTE F F F T F F F T) = BYTE T F F T T F F T) /\
  (GF256_by_9 (BYTE F F F T F F T F) = BYTE T F F F F F T F) /\
  (GF256_by_9 (BYTE F F F T F F T T) = BYTE T F F F T F T T) /\
  (GF256_by_9 (BYTE F F F T F T F F) = BYTE T F T T F T F F) /\
  (GF256_by_9 (BYTE F F F T F T F T) = BYTE T F T T T T F T) /\
  (GF256_by_9 (BYTE F F F T F T T F) = BYTE T F T F F T T F) /\
  (GF256_by_9 (BYTE F F F T F T T T) = BYTE T F T F T T T T) /\
  (GF256_by_9 (BYTE F F F T T F F F) = BYTE T T F T T F F F) /\
  (GF256_by_9 (BYTE F F F T T F F T) = BYTE T T F T F F F T) /\
  (GF256_by_9 (BYTE F F F T T F T F) = BYTE T T F F T F T F) /\
  (GF256_by_9 (BYTE F F F T T F T T) = BYTE T T F F F F T T) /\
  (GF256_by_9 (BYTE F F F T T T F F) = BYTE T T T T T T F F) /\
  (GF256_by_9 (BYTE F F F T T T F T) = BYTE T T T T F T F T) /\
  (GF256_by_9 (BYTE F F F T T T T F) = BYTE T T T F T T T F) /\
  (GF256_by_9 (BYTE F F F T T T T T) = BYTE T T T F F T T T) /\
  (GF256_by_9 (BYTE F F T F F F F F) = BYTE F F T T T F T T) /\
  (GF256_by_9 (BYTE F F T F F F F T) = BYTE F F T T F F T F) /\
  (GF256_by_9 (BYTE F F T F F F T F) = BYTE F F T F T F F T) /\
  (GF256_by_9 (BYTE F F T F F F T T) = BYTE F F T F F F F F) /\
  (GF256_by_9 (BYTE F F T F F T F F) = BYTE F F F T T T T T) /\
  (GF256_by_9 (BYTE F F T F F T F T) = BYTE F F F T F T T F) /\
  (GF256_by_9 (BYTE F F T F F T T F) = BYTE F F F F T T F T) /\
  (GF256_by_9 (BYTE F F T F F T T T) = BYTE F F F F F T F F) /\
  (GF256_by_9 (BYTE F F T F T F F F) = BYTE F T T T F F T T) /\
  (GF256_by_9 (BYTE F F T F T F F T) = BYTE F T T T T F T F) /\
  (GF256_by_9 (BYTE F F T F T F T F) = BYTE F T T F F F F T) /\
  (GF256_by_9 (BYTE F F T F T F T T) = BYTE F T T F T F F F) /\
  (GF256_by_9 (BYTE F F T F T T F F) = BYTE F T F T F T T T) /\
  (GF256_by_9 (BYTE F F T F T T F T) = BYTE F T F T T T T F) /\
  (GF256_by_9 (BYTE F F T F T T T F) = BYTE F T F F F T F T) /\
  (GF256_by_9 (BYTE F F T F T T T T) = BYTE F T F F T T F F) /\
  (GF256_by_9 (BYTE F F T T F F F F) = BYTE T F T F T F T T) /\
  (GF256_by_9 (BYTE F F T T F F F T) = BYTE T F T F F F T F) /\
  (GF256_by_9 (BYTE F F T T F F T F) = BYTE T F T T T F F T) /\
  (GF256_by_9 (BYTE F F T T F F T T) = BYTE T F T T F F F F) /\
  (GF256_by_9 (BYTE F F T T F T F F) = BYTE T F F F T T T T) /\
  (GF256_by_9 (BYTE F F T T F T F T) = BYTE T F F F F T T F) /\
  (GF256_by_9 (BYTE F F T T F T T F) = BYTE T F F T T T F T) /\
  (GF256_by_9 (BYTE F F T T F T T T) = BYTE T F F T F T F F) /\
  (GF256_by_9 (BYTE F F T T T F F F) = BYTE T T T F F F T T) /\
  (GF256_by_9 (BYTE F F T T T F F T) = BYTE T T T F T F T F) /\
  (GF256_by_9 (BYTE F F T T T F T F) = BYTE T T T T F F F T) /\
  (GF256_by_9 (BYTE F F T T T F T T) = BYTE T T T T T F F F) /\
  (GF256_by_9 (BYTE F F T T T T F F) = BYTE T T F F F T T T) /\
  (GF256_by_9 (BYTE F F T T T T F T) = BYTE T T F F T T T F) /\
  (GF256_by_9 (BYTE F F T T T T T F) = BYTE T T F T F T F T) /\
  (GF256_by_9 (BYTE F F T T T T T T) = BYTE T T F T T T F F) /\
  (GF256_by_9 (BYTE F T F F F F F F) = BYTE F T T T F T T F) /\
  (GF256_by_9 (BYTE F T F F F F F T) = BYTE F T T T T T T T) /\
  (GF256_by_9 (BYTE F T F F F F T F) = BYTE F T T F F T F F) /\
  (GF256_by_9 (BYTE F T F F F F T T) = BYTE F T T F T T F T) /\
  (GF256_by_9 (BYTE F T F F F T F F) = BYTE F T F T F F T F) /\
  (GF256_by_9 (BYTE F T F F F T F T) = BYTE F T F T T F T T) /\
  (GF256_by_9 (BYTE F T F F F T T F) = BYTE F T F F F F F F) /\
  (GF256_by_9 (BYTE F T F F F T T T) = BYTE F T F F T F F T) /\
  (GF256_by_9 (BYTE F T F F T F F F) = BYTE F F T T T T T F) /\
  (GF256_by_9 (BYTE F T F F T F F T) = BYTE F F T T F T T T) /\
  (GF256_by_9 (BYTE F T F F T F T F) = BYTE F F T F T T F F) /\
  (GF256_by_9 (BYTE F T F F T F T T) = BYTE F F T F F T F T) /\
  (GF256_by_9 (BYTE F T F F T T F F) = BYTE F F F T T F T F) /\
  (GF256_by_9 (BYTE F T F F T T F T) = BYTE F F F T F F T T) /\
  (GF256_by_9 (BYTE F T F F T T T F) = BYTE F F F F T F F F) /\
  (GF256_by_9 (BYTE F T F F T T T T) = BYTE F F F F F F F T) /\
  (GF256_by_9 (BYTE F T F T F F F F) = BYTE T T T F F T T F) /\
  (GF256_by_9 (BYTE F T F T F F F T) = BYTE T T T F T T T T) /\
  (GF256_by_9 (BYTE F T F T F F T F) = BYTE T T T T F T F F) /\
  (GF256_by_9 (BYTE F T F T F F T T) = BYTE T T T T T T F T) /\
  (GF256_by_9 (BYTE F T F T F T F F) = BYTE T T F F F F T F) /\
  (GF256_by_9 (BYTE F T F T F T F T) = BYTE T T F F T F T T) /\
  (GF256_by_9 (BYTE F T F T F T T F) = BYTE T T F T F F F F) /\
  (GF256_by_9 (BYTE F T F T F T T T) = BYTE T T F T T F F T) /\
  (GF256_by_9 (BYTE F T F T T F F F) = BYTE T F T F T T T F) /\
  (GF256_by_9 (BYTE F T F T T F F T) = BYTE T F T F F T T T) /\
  (GF256_by_9 (BYTE F T F T T F T F) = BYTE T F T T T T F F) /\
  (GF256_by_9 (BYTE F T F T T F T T) = BYTE T F T T F T F T) /\
  (GF256_by_9 (BYTE F T F T T T F F) = BYTE T F F F T F T F) /\
  (GF256_by_9 (BYTE F T F T T T F T) = BYTE T F F F F F T T) /\
  (GF256_by_9 (BYTE F T F T T T T F) = BYTE T F F T T F F F) /\
  (GF256_by_9 (BYTE F T F T T T T T) = BYTE T F F T F F F T) /\
  (GF256_by_9 (BYTE F T T F F F F F) = BYTE F T F F T T F T) /\
  (GF256_by_9 (BYTE F T T F F F F T) = BYTE F T F F F T F F) /\
  (GF256_by_9 (BYTE F T T F F F T F) = BYTE F T F T T T T T) /\
  (GF256_by_9 (BYTE F T T F F F T T) = BYTE F T F T F T T F) /\
  (GF256_by_9 (BYTE F T T F F T F F) = BYTE F T T F T F F T) /\
  (GF256_by_9 (BYTE F T T F F T F T) = BYTE F T T F F F F F) /\
  (GF256_by_9 (BYTE F T T F F T T F) = BYTE F T T T T F T T) /\
  (GF256_by_9 (BYTE F T T F F T T T) = BYTE F T T T F F T F) /\
  (GF256_by_9 (BYTE F T T F T F F F) = BYTE F F F F F T F T) /\
  (GF256_by_9 (BYTE F T T F T F F T) = BYTE F F F F T T F F) /\
  (GF256_by_9 (BYTE F T T F T F T F) = BYTE F F F T F T T T) /\
  (GF256_by_9 (BYTE F T T F T F T T) = BYTE F F F T T T T F) /\
  (GF256_by_9 (BYTE F T T F T T F F) = BYTE F F T F F F F T) /\
  (GF256_by_9 (BYTE F T T F T T F T) = BYTE F F T F T F F F) /\
  (GF256_by_9 (BYTE F T T F T T T F) = BYTE F F T T F F T T) /\
  (GF256_by_9 (BYTE F T T F T T T T) = BYTE F F T T T F T F) /\
  (GF256_by_9 (BYTE F T T T F F F F) = BYTE T T F T T T F T) /\
  (GF256_by_9 (BYTE F T T T F F F T) = BYTE T T F T F T F F) /\
  (GF256_by_9 (BYTE F T T T F F T F) = BYTE T T F F T T T T) /\
  (GF256_by_9 (BYTE F T T T F F T T) = BYTE T T F F F T T F) /\
  (GF256_by_9 (BYTE F T T T F T F F) = BYTE T T T T T F F T) /\
  (GF256_by_9 (BYTE F T T T F T F T) = BYTE T T T T F F F F) /\
  (GF256_by_9 (BYTE F T T T F T T F) = BYTE T T T F T F T T) /\
  (GF256_by_9 (BYTE F T T T F T T T) = BYTE T T T F F F T F) /\
  (GF256_by_9 (BYTE F T T T T F F F) = BYTE T F F T F T F T) /\
  (GF256_by_9 (BYTE F T T T T F F T) = BYTE T F F T T T F F) /\
  (GF256_by_9 (BYTE F T T T T F T F) = BYTE T F F F F T T T) /\
  (GF256_by_9 (BYTE F T T T T F T T) = BYTE T F F F T T T F) /\
  (GF256_by_9 (BYTE F T T T T T F F) = BYTE T F T T F F F T) /\
  (GF256_by_9 (BYTE F T T T T T F T) = BYTE T F T T T F F F) /\
  (GF256_by_9 (BYTE F T T T T T T F) = BYTE T F T F F F T T) /\
  (GF256_by_9 (BYTE F T T T T T T T) = BYTE T F T F T F T F) /\
  (GF256_by_9 (BYTE T F F F F F F F) = BYTE T T T F T T F F) /\
  (GF256_by_9 (BYTE T F F F F F F T) = BYTE T T T F F T F T) /\
  (GF256_by_9 (BYTE T F F F F F T F) = BYTE T T T T T T T F) /\
  (GF256_by_9 (BYTE T F F F F F T T) = BYTE T T T T F T T T) /\
  (GF256_by_9 (BYTE T F F F F T F F) = BYTE T T F F T F F F) /\
  (GF256_by_9 (BYTE T F F F F T F T) = BYTE T T F F F F F T) /\
  (GF256_by_9 (BYTE T F F F F T T F) = BYTE T T F T T F T F) /\
  (GF256_by_9 (BYTE T F F F F T T T) = BYTE T T F T F F T T) /\
  (GF256_by_9 (BYTE T F F F T F F F) = BYTE T F T F F T F F) /\
  (GF256_by_9 (BYTE T F F F T F F T) = BYTE T F T F T T F T) /\
  (GF256_by_9 (BYTE T F F F T F T F) = BYTE T F T T F T T F) /\
  (GF256_by_9 (BYTE T F F F T F T T) = BYTE T F T T T T T T) /\
  (GF256_by_9 (BYTE T F F F T T F F) = BYTE T F F F F F F F) /\
  (GF256_by_9 (BYTE T F F F T T F T) = BYTE T F F F T F F T) /\
  (GF256_by_9 (BYTE T F F F T T T F) = BYTE T F F T F F T F) /\
  (GF256_by_9 (BYTE T F F F T T T T) = BYTE T F F T T F T T) /\
  (GF256_by_9 (BYTE T F F T F F F F) = BYTE F T T T T T F F) /\
  (GF256_by_9 (BYTE T F F T F F F T) = BYTE F T T T F T F T) /\
  (GF256_by_9 (BYTE T F F T F F T F) = BYTE F T T F T T T F) /\
  (GF256_by_9 (BYTE T F F T F F T T) = BYTE F T T F F T T T) /\
  (GF256_by_9 (BYTE T F F T F T F F) = BYTE F T F T T F F F) /\
  (GF256_by_9 (BYTE T F F T F T F T) = BYTE F T F T F F F T) /\
  (GF256_by_9 (BYTE T F F T F T T F) = BYTE F T F F T F T F) /\
  (GF256_by_9 (BYTE T F F T F T T T) = BYTE F T F F F F T T) /\
  (GF256_by_9 (BYTE T F F T T F F F) = BYTE F F T T F T F F) /\
  (GF256_by_9 (BYTE T F F T T F F T) = BYTE F F T T T T F T) /\
  (GF256_by_9 (BYTE T F F T T F T F) = BYTE F F T F F T T F) /\
  (GF256_by_9 (BYTE T F F T T F T T) = BYTE F F T F T T T T) /\
  (GF256_by_9 (BYTE T F F T T T F F) = BYTE F F F T F F F F) /\
  (GF256_by_9 (BYTE T F F T T T F T) = BYTE F F F T T F F T) /\
  (GF256_by_9 (BYTE T F F T T T T F) = BYTE F F F F F F T F) /\
  (GF256_by_9 (BYTE T F F T T T T T) = BYTE F F F F T F T T) /\
  (GF256_by_9 (BYTE T F T F F F F F) = BYTE T T F T F T T T) /\
  (GF256_by_9 (BYTE T F T F F F F T) = BYTE T T F T T T T F) /\
  (GF256_by_9 (BYTE T F T F F F T F) = BYTE T T F F F T F T) /\
  (GF256_by_9 (BYTE T F T F F F T T) = BYTE T T F F T T F F) /\
  (GF256_by_9 (BYTE T F T F F T F F) = BYTE T T T T F F T T) /\
  (GF256_by_9 (BYTE T F T F F T F T) = BYTE T T T T T F T F) /\
  (GF256_by_9 (BYTE T F T F F T T F) = BYTE T T T F F F F T) /\
  (GF256_by_9 (BYTE T F T F F T T T) = BYTE T T T F T F F F) /\
  (GF256_by_9 (BYTE T F T F T F F F) = BYTE T F F T T T T T) /\
  (GF256_by_9 (BYTE T F T F T F F T) = BYTE T F F T F T T F) /\
  (GF256_by_9 (BYTE T F T F T F T F) = BYTE T F F F T T F T) /\
  (GF256_by_9 (BYTE T F T F T F T T) = BYTE T F F F F T F F) /\
  (GF256_by_9 (BYTE T F T F T T F F) = BYTE T F T T T F T T) /\
  (GF256_by_9 (BYTE T F T F T T F T) = BYTE T F T T F F T F) /\
  (GF256_by_9 (BYTE T F T F T T T F) = BYTE T F T F T F F T) /\
  (GF256_by_9 (BYTE T F T F T T T T) = BYTE T F T F F F F F) /\
  (GF256_by_9 (BYTE T F T T F F F F) = BYTE F T F F F T T T) /\
  (GF256_by_9 (BYTE T F T T F F F T) = BYTE F T F F T T T F) /\
  (GF256_by_9 (BYTE T F T T F F T F) = BYTE F T F T F T F T) /\
  (GF256_by_9 (BYTE T F T T F F T T) = BYTE F T F T T T F F) /\
  (GF256_by_9 (BYTE T F T T F T F F) = BYTE F T T F F F T T) /\
  (GF256_by_9 (BYTE T F T T F T F T) = BYTE F T T F T F T F) /\
  (GF256_by_9 (BYTE T F T T F T T F) = BYTE F T T T F F F T) /\
  (GF256_by_9 (BYTE T F T T F T T T) = BYTE F T T T T F F F) /\
  (GF256_by_9 (BYTE T F T T T F F F) = BYTE F F F F T T T T) /\
  (GF256_by_9 (BYTE T F T T T F F T) = BYTE F F F F F T T F) /\
  (GF256_by_9 (BYTE T F T T T F T F) = BYTE F F F T T T F T) /\
  (GF256_by_9 (BYTE T F T T T F T T) = BYTE F F F T F T F F) /\
  (GF256_by_9 (BYTE T F T T T T F F) = BYTE F F T F T F T T) /\
  (GF256_by_9 (BYTE T F T T T T F T) = BYTE F F T F F F T F) /\
  (GF256_by_9 (BYTE T F T T T T T F) = BYTE F F T T T F F T) /\
  (GF256_by_9 (BYTE T F T T T T T T) = BYTE F F T T F F F F) /\
  (GF256_by_9 (BYTE T T F F F F F F) = BYTE T F F T T F T F) /\
  (GF256_by_9 (BYTE T T F F F F F T) = BYTE T F F T F F T T) /\
  (GF256_by_9 (BYTE T T F F F F T F) = BYTE T F F F T F F F) /\
  (GF256_by_9 (BYTE T T F F F F T T) = BYTE T F F F F F F T) /\
  (GF256_by_9 (BYTE T T F F F T F F) = BYTE T F T T T T T F) /\
  (GF256_by_9 (BYTE T T F F F T F T) = BYTE T F T T F T T T) /\
  (GF256_by_9 (BYTE T T F F F T T F) = BYTE T F T F T T F F) /\
  (GF256_by_9 (BYTE T T F F F T T T) = BYTE T F T F F T F T) /\
  (GF256_by_9 (BYTE T T F F T F F F) = BYTE T T F T F F T F) /\
  (GF256_by_9 (BYTE T T F F T F F T) = BYTE T T F T T F T T) /\
  (GF256_by_9 (BYTE T T F F T F T F) = BYTE T T F F F F F F) /\
  (GF256_by_9 (BYTE T T F F T F T T) = BYTE T T F F T F F T) /\
  (GF256_by_9 (BYTE T T F F T T F F) = BYTE T T T T F T T F) /\
  (GF256_by_9 (BYTE T T F F T T F T) = BYTE T T T T T T T T) /\
  (GF256_by_9 (BYTE T T F F T T T F) = BYTE T T T F F T F F) /\
  (GF256_by_9 (BYTE T T F F T T T T) = BYTE T T T F T T F T) /\
  (GF256_by_9 (BYTE T T F T F F F F) = BYTE F F F F T F T F) /\
  (GF256_by_9 (BYTE T T F T F F F T) = BYTE F F F F F F T T) /\
  (GF256_by_9 (BYTE T T F T F F T F) = BYTE F F F T T F F F) /\
  (GF256_by_9 (BYTE T T F T F F T T) = BYTE F F F T F F F T) /\
  (GF256_by_9 (BYTE T T F T F T F F) = BYTE F F T F T T T F) /\
  (GF256_by_9 (BYTE T T F T F T F T) = BYTE F F T F F T T T) /\
  (GF256_by_9 (BYTE T T F T F T T F) = BYTE F F T T T T F F) /\
  (GF256_by_9 (BYTE T T F T F T T T) = BYTE F F T T F T F T) /\
  (GF256_by_9 (BYTE T T F T T F F F) = BYTE F T F F F F T F) /\
  (GF256_by_9 (BYTE T T F T T F F T) = BYTE F T F F T F T T) /\
  (GF256_by_9 (BYTE T T F T T F T F) = BYTE F T F T F F F F) /\
  (GF256_by_9 (BYTE T T F T T F T T) = BYTE F T F T T F F T) /\
  (GF256_by_9 (BYTE T T F T T T F F) = BYTE F T T F F T T F) /\
  (GF256_by_9 (BYTE T T F T T T F T) = BYTE F T T F T T T T) /\
  (GF256_by_9 (BYTE T T F T T T T F) = BYTE F T T T F T F F) /\
  (GF256_by_9 (BYTE T T F T T T T T) = BYTE F T T T T T F T) /\
  (GF256_by_9 (BYTE T T T F F F F F) = BYTE T F T F F F F T) /\
  (GF256_by_9 (BYTE T T T F F F F T) = BYTE T F T F T F F F) /\
  (GF256_by_9 (BYTE T T T F F F T F) = BYTE T F T T F F T T) /\
  (GF256_by_9 (BYTE T T T F F F T T) = BYTE T F T T T F T F) /\
  (GF256_by_9 (BYTE T T T F F T F F) = BYTE T F F F F T F T) /\
  (GF256_by_9 (BYTE T T T F F T F T) = BYTE T F F F T T F F) /\
  (GF256_by_9 (BYTE T T T F F T T F) = BYTE T F F T F T T T) /\
  (GF256_by_9 (BYTE T T T F F T T T) = BYTE T F F T T T T F) /\
  (GF256_by_9 (BYTE T T T F T F F F) = BYTE T T T F T F F T) /\
  (GF256_by_9 (BYTE T T T F T F F T) = BYTE T T T F F F F F) /\
  (GF256_by_9 (BYTE T T T F T F T F) = BYTE T T T T T F T T) /\
  (GF256_by_9 (BYTE T T T F T F T T) = BYTE T T T T F F T F) /\
  (GF256_by_9 (BYTE T T T F T T F F) = BYTE T T F F T T F T) /\
  (GF256_by_9 (BYTE T T T F T T F T) = BYTE T T F F F T F F) /\
  (GF256_by_9 (BYTE T T T F T T T F) = BYTE T T F T T T T T) /\
  (GF256_by_9 (BYTE T T T F T T T T) = BYTE T T F T F T T F) /\
  (GF256_by_9 (BYTE T T T T F F F F) = BYTE F F T T F F F T) /\
  (GF256_by_9 (BYTE T T T T F F F T) = BYTE F F T T T F F F) /\
  (GF256_by_9 (BYTE T T T T F F T F) = BYTE F F T F F F T T) /\
  (GF256_by_9 (BYTE T T T T F F T T) = BYTE F F T F T F T F) /\
  (GF256_by_9 (BYTE T T T T F T F F) = BYTE F F F T F T F T) /\
  (GF256_by_9 (BYTE T T T T F T F T) = BYTE F F F T T T F F) /\
  (GF256_by_9 (BYTE T T T T F T T F) = BYTE F F F F F T T T) /\
  (GF256_by_9 (BYTE T T T T F T T T) = BYTE F F F F T T T F) /\
  (GF256_by_9 (BYTE T T T T T F F F) = BYTE F T T T T F F T) /\
  (GF256_by_9 (BYTE T T T T T F F T) = BYTE F T T T F F F F) /\
  (GF256_by_9 (BYTE T T T T T F T F) = BYTE F T T F T F T T) /\
  (GF256_by_9 (BYTE T T T T T F T T) = BYTE F T T F F F T F) /\
  (GF256_by_9 (BYTE T T T T T T F F) = BYTE F T F T T T F T) /\
  (GF256_by_9 (BYTE T T T T T T F T) = BYTE F T F T F T F F) /\
  (GF256_by_9 (BYTE T T T T T T T F) = BYTE F T F F T T T T) /\
  (GF256_by_9 (BYTE T T T T T T T T) = BYTE F T F F F T T F)`;

val GF256_by_11_def = Count.apply Define
 `(GF256_by_11 (BYTE F F F F F F F F) = BYTE F F F F F F F F) /\
  (GF256_by_11 (BYTE F F F F F F F T) = BYTE F F F F T F T T) /\
  (GF256_by_11 (BYTE F F F F F F T F) = BYTE F F F T F T T F) /\
  (GF256_by_11 (BYTE F F F F F F T T) = BYTE F F F T T T F T) /\
  (GF256_by_11 (BYTE F F F F F T F F) = BYTE F F T F T T F F) /\
  (GF256_by_11 (BYTE F F F F F T F T) = BYTE F F T F F T T T) /\
  (GF256_by_11 (BYTE F F F F F T T F) = BYTE F F T T T F T F) /\
  (GF256_by_11 (BYTE F F F F F T T T) = BYTE F F T T F F F T) /\
  (GF256_by_11 (BYTE F F F F T F F F) = BYTE F T F T T F F F) /\
  (GF256_by_11 (BYTE F F F F T F F T) = BYTE F T F T F F T T) /\
  (GF256_by_11 (BYTE F F F F T F T F) = BYTE F T F F T T T F) /\
  (GF256_by_11 (BYTE F F F F T F T T) = BYTE F T F F F T F T) /\
  (GF256_by_11 (BYTE F F F F T T F F) = BYTE F T T T F T F F) /\
  (GF256_by_11 (BYTE F F F F T T F T) = BYTE F T T T T T T T) /\
  (GF256_by_11 (BYTE F F F F T T T F) = BYTE F T T F F F T F) /\
  (GF256_by_11 (BYTE F F F F T T T T) = BYTE F T T F T F F T) /\
  (GF256_by_11 (BYTE F F F T F F F F) = BYTE T F T T F F F F) /\
  (GF256_by_11 (BYTE F F F T F F F T) = BYTE T F T T T F T T) /\
  (GF256_by_11 (BYTE F F F T F F T F) = BYTE T F T F F T T F) /\
  (GF256_by_11 (BYTE F F F T F F T T) = BYTE T F T F T T F T) /\
  (GF256_by_11 (BYTE F F F T F T F F) = BYTE T F F T T T F F) /\
  (GF256_by_11 (BYTE F F F T F T F T) = BYTE T F F T F T T T) /\
  (GF256_by_11 (BYTE F F F T F T T F) = BYTE T F F F T F T F) /\
  (GF256_by_11 (BYTE F F F T F T T T) = BYTE T F F F F F F T) /\
  (GF256_by_11 (BYTE F F F T T F F F) = BYTE T T T F T F F F) /\
  (GF256_by_11 (BYTE F F F T T F F T) = BYTE T T T F F F T T) /\
  (GF256_by_11 (BYTE F F F T T F T F) = BYTE T T T T T T T F) /\
  (GF256_by_11 (BYTE F F F T T F T T) = BYTE T T T T F T F T) /\
  (GF256_by_11 (BYTE F F F T T T F F) = BYTE T T F F F T F F) /\
  (GF256_by_11 (BYTE F F F T T T F T) = BYTE T T F F T T T T) /\
  (GF256_by_11 (BYTE F F F T T T T F) = BYTE T T F T F F T F) /\
  (GF256_by_11 (BYTE F F F T T T T T) = BYTE T T F T T F F T) /\
  (GF256_by_11 (BYTE F F T F F F F F) = BYTE F T T T T F T T) /\
  (GF256_by_11 (BYTE F F T F F F F T) = BYTE F T T T F F F F) /\
  (GF256_by_11 (BYTE F F T F F F T F) = BYTE F T T F T T F T) /\
  (GF256_by_11 (BYTE F F T F F F T T) = BYTE F T T F F T T F) /\
  (GF256_by_11 (BYTE F F T F F T F F) = BYTE F T F T F T T T) /\
  (GF256_by_11 (BYTE F F T F F T F T) = BYTE F T F T T T F F) /\
  (GF256_by_11 (BYTE F F T F F T T F) = BYTE F T F F F F F T) /\
  (GF256_by_11 (BYTE F F T F F T T T) = BYTE F T F F T F T F) /\
  (GF256_by_11 (BYTE F F T F T F F F) = BYTE F F T F F F T T) /\
  (GF256_by_11 (BYTE F F T F T F F T) = BYTE F F T F T F F F) /\
  (GF256_by_11 (BYTE F F T F T F T F) = BYTE F F T T F T F T) /\
  (GF256_by_11 (BYTE F F T F T F T T) = BYTE F F T T T T T F) /\
  (GF256_by_11 (BYTE F F T F T T F F) = BYTE F F F F T T T T) /\
  (GF256_by_11 (BYTE F F T F T T F T) = BYTE F F F F F T F F) /\
  (GF256_by_11 (BYTE F F T F T T T F) = BYTE F F F T T F F T) /\
  (GF256_by_11 (BYTE F F T F T T T T) = BYTE F F F T F F T F) /\
  (GF256_by_11 (BYTE F F T T F F F F) = BYTE T T F F T F T T) /\
  (GF256_by_11 (BYTE F F T T F F F T) = BYTE T T F F F F F F) /\
  (GF256_by_11 (BYTE F F T T F F T F) = BYTE T T F T T T F T) /\
  (GF256_by_11 (BYTE F F T T F F T T) = BYTE T T F T F T T F) /\
  (GF256_by_11 (BYTE F F T T F T F F) = BYTE T T T F F T T T) /\
  (GF256_by_11 (BYTE F F T T F T F T) = BYTE T T T F T T F F) /\
  (GF256_by_11 (BYTE F F T T F T T F) = BYTE T T T T F F F T) /\
  (GF256_by_11 (BYTE F F T T F T T T) = BYTE T T T T T F T F) /\
  (GF256_by_11 (BYTE F F T T T F F F) = BYTE T F F T F F T T) /\
  (GF256_by_11 (BYTE F F T T T F F T) = BYTE T F F T T F F F) /\
  (GF256_by_11 (BYTE F F T T T F T F) = BYTE T F F F F T F T) /\
  (GF256_by_11 (BYTE F F T T T F T T) = BYTE T F F F T T T F) /\
  (GF256_by_11 (BYTE F F T T T T F F) = BYTE T F T T T T T T) /\
  (GF256_by_11 (BYTE F F T T T T F T) = BYTE T F T T F T F F) /\
  (GF256_by_11 (BYTE F F T T T T T F) = BYTE T F T F T F F T) /\
  (GF256_by_11 (BYTE F F T T T T T T) = BYTE T F T F F F T F) /\
  (GF256_by_11 (BYTE F T F F F F F F) = BYTE T T T T F T T F) /\
  (GF256_by_11 (BYTE F T F F F F F T) = BYTE T T T T T T F T) /\
  (GF256_by_11 (BYTE F T F F F F T F) = BYTE T T T F F F F F) /\
  (GF256_by_11 (BYTE F T F F F F T T) = BYTE T T T F T F T T) /\
  (GF256_by_11 (BYTE F T F F F T F F) = BYTE T T F T T F T F) /\
  (GF256_by_11 (BYTE F T F F F T F T) = BYTE T T F T F F F T) /\
  (GF256_by_11 (BYTE F T F F F T T F) = BYTE T T F F T T F F) /\
  (GF256_by_11 (BYTE F T F F F T T T) = BYTE T T F F F T T T) /\
  (GF256_by_11 (BYTE F T F F T F F F) = BYTE T F T F T T T F) /\
  (GF256_by_11 (BYTE F T F F T F F T) = BYTE T F T F F T F T) /\
  (GF256_by_11 (BYTE F T F F T F T F) = BYTE T F T T T F F F) /\
  (GF256_by_11 (BYTE F T F F T F T T) = BYTE T F T T F F T T) /\
  (GF256_by_11 (BYTE F T F F T T F F) = BYTE T F F F F F T F) /\
  (GF256_by_11 (BYTE F T F F T T F T) = BYTE T F F F T F F T) /\
  (GF256_by_11 (BYTE F T F F T T T F) = BYTE T F F T F T F F) /\
  (GF256_by_11 (BYTE F T F F T T T T) = BYTE T F F T T T T T) /\
  (GF256_by_11 (BYTE F T F T F F F F) = BYTE F T F F F T T F) /\
  (GF256_by_11 (BYTE F T F T F F F T) = BYTE F T F F T T F T) /\
  (GF256_by_11 (BYTE F T F T F F T F) = BYTE F T F T F F F F) /\
  (GF256_by_11 (BYTE F T F T F F T T) = BYTE F T F T T F T T) /\
  (GF256_by_11 (BYTE F T F T F T F F) = BYTE F T T F T F T F) /\
  (GF256_by_11 (BYTE F T F T F T F T) = BYTE F T T F F F F T) /\
  (GF256_by_11 (BYTE F T F T F T T F) = BYTE F T T T T T F F) /\
  (GF256_by_11 (BYTE F T F T F T T T) = BYTE F T T T F T T T) /\
  (GF256_by_11 (BYTE F T F T T F F F) = BYTE F F F T T T T F) /\
  (GF256_by_11 (BYTE F T F T T F F T) = BYTE F F F T F T F T) /\
  (GF256_by_11 (BYTE F T F T T F T F) = BYTE F F F F T F F F) /\
  (GF256_by_11 (BYTE F T F T T F T T) = BYTE F F F F F F T T) /\
  (GF256_by_11 (BYTE F T F T T T F F) = BYTE F F T T F F T F) /\
  (GF256_by_11 (BYTE F T F T T T F T) = BYTE F F T T T F F T) /\
  (GF256_by_11 (BYTE F T F T T T T F) = BYTE F F T F F T F F) /\
  (GF256_by_11 (BYTE F T F T T T T T) = BYTE F F T F T T T T) /\
  (GF256_by_11 (BYTE F T T F F F F F) = BYTE T F F F T T F T) /\
  (GF256_by_11 (BYTE F T T F F F F T) = BYTE T F F F F T T F) /\
  (GF256_by_11 (BYTE F T T F F F T F) = BYTE T F F T T F T T) /\
  (GF256_by_11 (BYTE F T T F F F T T) = BYTE T F F T F F F F) /\
  (GF256_by_11 (BYTE F T T F F T F F) = BYTE T F T F F F F T) /\
  (GF256_by_11 (BYTE F T T F F T F T) = BYTE T F T F T F T F) /\
  (GF256_by_11 (BYTE F T T F F T T F) = BYTE T F T T F T T T) /\
  (GF256_by_11 (BYTE F T T F F T T T) = BYTE T F T T T T F F) /\
  (GF256_by_11 (BYTE F T T F T F F F) = BYTE T T F T F T F T) /\
  (GF256_by_11 (BYTE F T T F T F F T) = BYTE T T F T T T T F) /\
  (GF256_by_11 (BYTE F T T F T F T F) = BYTE T T F F F F T T) /\
  (GF256_by_11 (BYTE F T T F T F T T) = BYTE T T F F T F F F) /\
  (GF256_by_11 (BYTE F T T F T T F F) = BYTE T T T T T F F T) /\
  (GF256_by_11 (BYTE F T T F T T F T) = BYTE T T T T F F T F) /\
  (GF256_by_11 (BYTE F T T F T T T F) = BYTE T T T F T T T T) /\
  (GF256_by_11 (BYTE F T T F T T T T) = BYTE T T T F F T F F) /\
  (GF256_by_11 (BYTE F T T T F F F F) = BYTE F F T T T T F T) /\
  (GF256_by_11 (BYTE F T T T F F F T) = BYTE F F T T F T T F) /\
  (GF256_by_11 (BYTE F T T T F F T F) = BYTE F F T F T F T T) /\
  (GF256_by_11 (BYTE F T T T F F T T) = BYTE F F T F F F F F) /\
  (GF256_by_11 (BYTE F T T T F T F F) = BYTE F F F T F F F T) /\
  (GF256_by_11 (BYTE F T T T F T F T) = BYTE F F F T T F T F) /\
  (GF256_by_11 (BYTE F T T T F T T F) = BYTE F F F F F T T T) /\
  (GF256_by_11 (BYTE F T T T F T T T) = BYTE F F F F T T F F) /\
  (GF256_by_11 (BYTE F T T T T F F F) = BYTE F T T F F T F T) /\
  (GF256_by_11 (BYTE F T T T T F F T) = BYTE F T T F T T T F) /\
  (GF256_by_11 (BYTE F T T T T F T F) = BYTE F T T T F F T T) /\
  (GF256_by_11 (BYTE F T T T T F T T) = BYTE F T T T T F F F) /\
  (GF256_by_11 (BYTE F T T T T T F F) = BYTE F T F F T F F T) /\
  (GF256_by_11 (BYTE F T T T T T F T) = BYTE F T F F F F T F) /\
  (GF256_by_11 (BYTE F T T T T T T F) = BYTE F T F T T T T T) /\
  (GF256_by_11 (BYTE F T T T T T T T) = BYTE F T F T F T F F) /\
  (GF256_by_11 (BYTE T F F F F F F F) = BYTE T T T T F T T T) /\
  (GF256_by_11 (BYTE T F F F F F F T) = BYTE T T T T T T F F) /\
  (GF256_by_11 (BYTE T F F F F F T F) = BYTE T T T F F F F T) /\
  (GF256_by_11 (BYTE T F F F F F T T) = BYTE T T T F T F T F) /\
  (GF256_by_11 (BYTE T F F F F T F F) = BYTE T T F T T F T T) /\
  (GF256_by_11 (BYTE T F F F F T F T) = BYTE T T F T F F F F) /\
  (GF256_by_11 (BYTE T F F F F T T F) = BYTE T T F F T T F T) /\
  (GF256_by_11 (BYTE T F F F F T T T) = BYTE T T F F F T T F) /\
  (GF256_by_11 (BYTE T F F F T F F F) = BYTE T F T F T T T T) /\
  (GF256_by_11 (BYTE T F F F T F F T) = BYTE T F T F F T F F) /\
  (GF256_by_11 (BYTE T F F F T F T F) = BYTE T F T T T F F T) /\
  (GF256_by_11 (BYTE T F F F T F T T) = BYTE T F T T F F T F) /\
  (GF256_by_11 (BYTE T F F F T T F F) = BYTE T F F F F F T T) /\
  (GF256_by_11 (BYTE T F F F T T F T) = BYTE T F F F T F F F) /\
  (GF256_by_11 (BYTE T F F F T T T F) = BYTE T F F T F T F T) /\
  (GF256_by_11 (BYTE T F F F T T T T) = BYTE T F F T T T T F) /\
  (GF256_by_11 (BYTE T F F T F F F F) = BYTE F T F F F T T T) /\
  (GF256_by_11 (BYTE T F F T F F F T) = BYTE F T F F T T F F) /\
  (GF256_by_11 (BYTE T F F T F F T F) = BYTE F T F T F F F T) /\
  (GF256_by_11 (BYTE T F F T F F T T) = BYTE F T F T T F T F) /\
  (GF256_by_11 (BYTE T F F T F T F F) = BYTE F T T F T F T T) /\
  (GF256_by_11 (BYTE T F F T F T F T) = BYTE F T T F F F F F) /\
  (GF256_by_11 (BYTE T F F T F T T F) = BYTE F T T T T T F T) /\
  (GF256_by_11 (BYTE T F F T F T T T) = BYTE F T T T F T T F) /\
  (GF256_by_11 (BYTE T F F T T F F F) = BYTE F F F T T T T T) /\
  (GF256_by_11 (BYTE T F F T T F F T) = BYTE F F F T F T F F) /\
  (GF256_by_11 (BYTE T F F T T F T F) = BYTE F F F F T F F T) /\
  (GF256_by_11 (BYTE T F F T T F T T) = BYTE F F F F F F T F) /\
  (GF256_by_11 (BYTE T F F T T T F F) = BYTE F F T T F F T T) /\
  (GF256_by_11 (BYTE T F F T T T F T) = BYTE F F T T T F F F) /\
  (GF256_by_11 (BYTE T F F T T T T F) = BYTE F F T F F T F T) /\
  (GF256_by_11 (BYTE T F F T T T T T) = BYTE F F T F T T T F) /\
  (GF256_by_11 (BYTE T F T F F F F F) = BYTE T F F F T T F F) /\
  (GF256_by_11 (BYTE T F T F F F F T) = BYTE T F F F F T T T) /\
  (GF256_by_11 (BYTE T F T F F F T F) = BYTE T F F T T F T F) /\
  (GF256_by_11 (BYTE T F T F F F T T) = BYTE T F F T F F F T) /\
  (GF256_by_11 (BYTE T F T F F T F F) = BYTE T F T F F F F F) /\
  (GF256_by_11 (BYTE T F T F F T F T) = BYTE T F T F T F T T) /\
  (GF256_by_11 (BYTE T F T F F T T F) = BYTE T F T T F T T F) /\
  (GF256_by_11 (BYTE T F T F F T T T) = BYTE T F T T T T F T) /\
  (GF256_by_11 (BYTE T F T F T F F F) = BYTE T T F T F T F F) /\
  (GF256_by_11 (BYTE T F T F T F F T) = BYTE T T F T T T T T) /\
  (GF256_by_11 (BYTE T F T F T F T F) = BYTE T T F F F F T F) /\
  (GF256_by_11 (BYTE T F T F T F T T) = BYTE T T F F T F F T) /\
  (GF256_by_11 (BYTE T F T F T T F F) = BYTE T T T T T F F F) /\
  (GF256_by_11 (BYTE T F T F T T F T) = BYTE T T T T F F T T) /\
  (GF256_by_11 (BYTE T F T F T T T F) = BYTE T T T F T T T F) /\
  (GF256_by_11 (BYTE T F T F T T T T) = BYTE T T T F F T F T) /\
  (GF256_by_11 (BYTE T F T T F F F F) = BYTE F F T T T T F F) /\
  (GF256_by_11 (BYTE T F T T F F F T) = BYTE F F T T F T T T) /\
  (GF256_by_11 (BYTE T F T T F F T F) = BYTE F F T F T F T F) /\
  (GF256_by_11 (BYTE T F T T F F T T) = BYTE F F T F F F F T) /\
  (GF256_by_11 (BYTE T F T T F T F F) = BYTE F F F T F F F F) /\
  (GF256_by_11 (BYTE T F T T F T F T) = BYTE F F F T T F T T) /\
  (GF256_by_11 (BYTE T F T T F T T F) = BYTE F F F F F T T F) /\
  (GF256_by_11 (BYTE T F T T F T T T) = BYTE F F F F T T F T) /\
  (GF256_by_11 (BYTE T F T T T F F F) = BYTE F T T F F T F F) /\
  (GF256_by_11 (BYTE T F T T T F F T) = BYTE F T T F T T T T) /\
  (GF256_by_11 (BYTE T F T T T F T F) = BYTE F T T T F F T F) /\
  (GF256_by_11 (BYTE T F T T T F T T) = BYTE F T T T T F F T) /\
  (GF256_by_11 (BYTE T F T T T T F F) = BYTE F T F F T F F F) /\
  (GF256_by_11 (BYTE T F T T T T F T) = BYTE F T F F F F T T) /\
  (GF256_by_11 (BYTE T F T T T T T F) = BYTE F T F T T T T F) /\
  (GF256_by_11 (BYTE T F T T T T T T) = BYTE F T F T F T F T) /\
  (GF256_by_11 (BYTE T T F F F F F F) = BYTE F F F F F F F T) /\
  (GF256_by_11 (BYTE T T F F F F F T) = BYTE F F F F T F T F) /\
  (GF256_by_11 (BYTE T T F F F F T F) = BYTE F F F T F T T T) /\
  (GF256_by_11 (BYTE T T F F F F T T) = BYTE F F F T T T F F) /\
  (GF256_by_11 (BYTE T T F F F T F F) = BYTE F F T F T T F T) /\
  (GF256_by_11 (BYTE T T F F F T F T) = BYTE F F T F F T T F) /\
  (GF256_by_11 (BYTE T T F F F T T F) = BYTE F F T T T F T T) /\
  (GF256_by_11 (BYTE T T F F F T T T) = BYTE F F T T F F F F) /\
  (GF256_by_11 (BYTE T T F F T F F F) = BYTE F T F T T F F T) /\
  (GF256_by_11 (BYTE T T F F T F F T) = BYTE F T F T F F T F) /\
  (GF256_by_11 (BYTE T T F F T F T F) = BYTE F T F F T T T T) /\
  (GF256_by_11 (BYTE T T F F T F T T) = BYTE F T F F F T F F) /\
  (GF256_by_11 (BYTE T T F F T T F F) = BYTE F T T T F T F T) /\
  (GF256_by_11 (BYTE T T F F T T F T) = BYTE F T T T T T T F) /\
  (GF256_by_11 (BYTE T T F F T T T F) = BYTE F T T F F F T T) /\
  (GF256_by_11 (BYTE T T F F T T T T) = BYTE F T T F T F F F) /\
  (GF256_by_11 (BYTE T T F T F F F F) = BYTE T F T T F F F T) /\
  (GF256_by_11 (BYTE T T F T F F F T) = BYTE T F T T T F T F) /\
  (GF256_by_11 (BYTE T T F T F F T F) = BYTE T F T F F T T T) /\
  (GF256_by_11 (BYTE T T F T F F T T) = BYTE T F T F T T F F) /\
  (GF256_by_11 (BYTE T T F T F T F F) = BYTE T F F T T T F T) /\
  (GF256_by_11 (BYTE T T F T F T F T) = BYTE T F F T F T T F) /\
  (GF256_by_11 (BYTE T T F T F T T F) = BYTE T F F F T F T T) /\
  (GF256_by_11 (BYTE T T F T F T T T) = BYTE T F F F F F F F) /\
  (GF256_by_11 (BYTE T T F T T F F F) = BYTE T T T F T F F T) /\
  (GF256_by_11 (BYTE T T F T T F F T) = BYTE T T T F F F T F) /\
  (GF256_by_11 (BYTE T T F T T F T F) = BYTE T T T T T T T T) /\
  (GF256_by_11 (BYTE T T F T T F T T) = BYTE T T T T F T F F) /\
  (GF256_by_11 (BYTE T T F T T T F F) = BYTE T T F F F T F T) /\
  (GF256_by_11 (BYTE T T F T T T F T) = BYTE T T F F T T T F) /\
  (GF256_by_11 (BYTE T T F T T T T F) = BYTE T T F T F F T T) /\
  (GF256_by_11 (BYTE T T F T T T T T) = BYTE T T F T T F F F) /\
  (GF256_by_11 (BYTE T T T F F F F F) = BYTE F T T T T F T F) /\
  (GF256_by_11 (BYTE T T T F F F F T) = BYTE F T T T F F F T) /\
  (GF256_by_11 (BYTE T T T F F F T F) = BYTE F T T F T T F F) /\
  (GF256_by_11 (BYTE T T T F F F T T) = BYTE F T T F F T T T) /\
  (GF256_by_11 (BYTE T T T F F T F F) = BYTE F T F T F T T F) /\
  (GF256_by_11 (BYTE T T T F F T F T) = BYTE F T F T T T F T) /\
  (GF256_by_11 (BYTE T T T F F T T F) = BYTE F T F F F F F F) /\
  (GF256_by_11 (BYTE T T T F F T T T) = BYTE F T F F T F T T) /\
  (GF256_by_11 (BYTE T T T F T F F F) = BYTE F F T F F F T F) /\
  (GF256_by_11 (BYTE T T T F T F F T) = BYTE F F T F T F F T) /\
  (GF256_by_11 (BYTE T T T F T F T F) = BYTE F F T T F T F F) /\
  (GF256_by_11 (BYTE T T T F T F T T) = BYTE F F T T T T T T) /\
  (GF256_by_11 (BYTE T T T F T T F F) = BYTE F F F F T T T F) /\
  (GF256_by_11 (BYTE T T T F T T F T) = BYTE F F F F F T F T) /\
  (GF256_by_11 (BYTE T T T F T T T F) = BYTE F F F T T F F F) /\
  (GF256_by_11 (BYTE T T T F T T T T) = BYTE F F F T F F T T) /\
  (GF256_by_11 (BYTE T T T T F F F F) = BYTE T T F F T F T F) /\
  (GF256_by_11 (BYTE T T T T F F F T) = BYTE T T F F F F F T) /\
  (GF256_by_11 (BYTE T T T T F F T F) = BYTE T T F T T T F F) /\
  (GF256_by_11 (BYTE T T T T F F T T) = BYTE T T F T F T T T) /\
  (GF256_by_11 (BYTE T T T T F T F F) = BYTE T T T F F T T F) /\
  (GF256_by_11 (BYTE T T T T F T F T) = BYTE T T T F T T F T) /\
  (GF256_by_11 (BYTE T T T T F T T F) = BYTE T T T T F F F F) /\
  (GF256_by_11 (BYTE T T T T F T T T) = BYTE T T T T T F T T) /\
  (GF256_by_11 (BYTE T T T T T F F F) = BYTE T F F T F F T F) /\
  (GF256_by_11 (BYTE T T T T T F F T) = BYTE T F F T T F F T) /\
  (GF256_by_11 (BYTE T T T T T F T F) = BYTE T F F F F T F F) /\
  (GF256_by_11 (BYTE T T T T T F T T) = BYTE T F F F T T T T) /\
  (GF256_by_11 (BYTE T T T T T T F F) = BYTE T F T T T T T F) /\
  (GF256_by_11 (BYTE T T T T T T F T) = BYTE T F T T F T F T) /\
  (GF256_by_11 (BYTE T T T T T T T F) = BYTE T F T F T F F F) /\
  (GF256_by_11 (BYTE T T T T T T T T) = BYTE T F T F F F T T)`;

val GF256_by_13_def = Count.apply Define
 `(GF256_by_13 (BYTE F F F F F F F F) = BYTE F F F F F F F F) /\
  (GF256_by_13 (BYTE F F F F F F F T) = BYTE F F F F T T F T) /\
  (GF256_by_13 (BYTE F F F F F F T F) = BYTE F F F T T F T F) /\
  (GF256_by_13 (BYTE F F F F F F T T) = BYTE F F F T F T T T) /\
  (GF256_by_13 (BYTE F F F F F T F F) = BYTE F F T T F T F F) /\
  (GF256_by_13 (BYTE F F F F F T F T) = BYTE F F T T T F F T) /\
  (GF256_by_13 (BYTE F F F F F T T F) = BYTE F F T F T T T F) /\
  (GF256_by_13 (BYTE F F F F F T T T) = BYTE F F T F F F T T) /\
  (GF256_by_13 (BYTE F F F F T F F F) = BYTE F T T F T F F F) /\
  (GF256_by_13 (BYTE F F F F T F F T) = BYTE F T T F F T F T) /\
  (GF256_by_13 (BYTE F F F F T F T F) = BYTE F T T T F F T F) /\
  (GF256_by_13 (BYTE F F F F T F T T) = BYTE F T T T T T T T) /\
  (GF256_by_13 (BYTE F F F F T T F F) = BYTE F T F T T T F F) /\
  (GF256_by_13 (BYTE F F F F T T F T) = BYTE F T F T F F F T) /\
  (GF256_by_13 (BYTE F F F F T T T F) = BYTE F T F F F T T F) /\
  (GF256_by_13 (BYTE F F F F T T T T) = BYTE F T F F T F T T) /\
  (GF256_by_13 (BYTE F F F T F F F F) = BYTE T T F T F F F F) /\
  (GF256_by_13 (BYTE F F F T F F F T) = BYTE T T F T T T F T) /\
  (GF256_by_13 (BYTE F F F T F F T F) = BYTE T T F F T F T F) /\
  (GF256_by_13 (BYTE F F F T F F T T) = BYTE T T F F F T T T) /\
  (GF256_by_13 (BYTE F F F T F T F F) = BYTE T T T F F T F F) /\
  (GF256_by_13 (BYTE F F F T F T F T) = BYTE T T T F T F F T) /\
  (GF256_by_13 (BYTE F F F T F T T F) = BYTE T T T T T T T F) /\
  (GF256_by_13 (BYTE F F F T F T T T) = BYTE T T T T F F T T) /\
  (GF256_by_13 (BYTE F F F T T F F F) = BYTE T F T T T F F F) /\
  (GF256_by_13 (BYTE F F F T T F F T) = BYTE T F T T F T F T) /\
  (GF256_by_13 (BYTE F F F T T F T F) = BYTE T F T F F F T F) /\
  (GF256_by_13 (BYTE F F F T T F T T) = BYTE T F T F T T T T) /\
  (GF256_by_13 (BYTE F F F T T T F F) = BYTE T F F F T T F F) /\
  (GF256_by_13 (BYTE F F F T T T F T) = BYTE T F F F F F F T) /\
  (GF256_by_13 (BYTE F F F T T T T F) = BYTE T F F T F T T F) /\
  (GF256_by_13 (BYTE F F F T T T T T) = BYTE T F F T T F T T) /\
  (GF256_by_13 (BYTE F F T F F F F F) = BYTE T F T T T F T T) /\
  (GF256_by_13 (BYTE F F T F F F F T) = BYTE T F T T F T T F) /\
  (GF256_by_13 (BYTE F F T F F F T F) = BYTE T F T F F F F T) /\
  (GF256_by_13 (BYTE F F T F F F T T) = BYTE T F T F T T F F) /\
  (GF256_by_13 (BYTE F F T F F T F F) = BYTE T F F F T T T T) /\
  (GF256_by_13 (BYTE F F T F F T F T) = BYTE T F F F F F T F) /\
  (GF256_by_13 (BYTE F F T F F T T F) = BYTE T F F T F T F T) /\
  (GF256_by_13 (BYTE F F T F F T T T) = BYTE T F F T T F F F) /\
  (GF256_by_13 (BYTE F F T F T F F F) = BYTE T T F T F F T T) /\
  (GF256_by_13 (BYTE F F T F T F F T) = BYTE T T F T T T T F) /\
  (GF256_by_13 (BYTE F F T F T F T F) = BYTE T T F F T F F T) /\
  (GF256_by_13 (BYTE F F T F T F T T) = BYTE T T F F F T F F) /\
  (GF256_by_13 (BYTE F F T F T T F F) = BYTE T T T F F T T T) /\
  (GF256_by_13 (BYTE F F T F T T F T) = BYTE T T T F T F T F) /\
  (GF256_by_13 (BYTE F F T F T T T F) = BYTE T T T T T T F T) /\
  (GF256_by_13 (BYTE F F T F T T T T) = BYTE T T T T F F F F) /\
  (GF256_by_13 (BYTE F F T T F F F F) = BYTE F T T F T F T T) /\
  (GF256_by_13 (BYTE F F T T F F F T) = BYTE F T T F F T T F) /\
  (GF256_by_13 (BYTE F F T T F F T F) = BYTE F T T T F F F T) /\
  (GF256_by_13 (BYTE F F T T F F T T) = BYTE F T T T T T F F) /\
  (GF256_by_13 (BYTE F F T T F T F F) = BYTE F T F T T T T T) /\
  (GF256_by_13 (BYTE F F T T F T F T) = BYTE F T F T F F T F) /\
  (GF256_by_13 (BYTE F F T T F T T F) = BYTE F T F F F T F T) /\
  (GF256_by_13 (BYTE F F T T F T T T) = BYTE F T F F T F F F) /\
  (GF256_by_13 (BYTE F F T T T F F F) = BYTE F F F F F F T T) /\
  (GF256_by_13 (BYTE F F T T T F F T) = BYTE F F F F T T T F) /\
  (GF256_by_13 (BYTE F F T T T F T F) = BYTE F F F T T F F T) /\
  (GF256_by_13 (BYTE F F T T T F T T) = BYTE F F F T F T F F) /\
  (GF256_by_13 (BYTE F F T T T T F F) = BYTE F F T T F T T T) /\
  (GF256_by_13 (BYTE F F T T T T F T) = BYTE F F T T T F T F) /\
  (GF256_by_13 (BYTE F F T T T T T F) = BYTE F F T F T T F T) /\
  (GF256_by_13 (BYTE F F T T T T T T) = BYTE F F T F F F F F) /\
  (GF256_by_13 (BYTE F T F F F F F F) = BYTE F T T F T T F T) /\
  (GF256_by_13 (BYTE F T F F F F F T) = BYTE F T T F F F F F) /\
  (GF256_by_13 (BYTE F T F F F F T F) = BYTE F T T T F T T T) /\
  (GF256_by_13 (BYTE F T F F F F T T) = BYTE F T T T T F T F) /\
  (GF256_by_13 (BYTE F T F F F T F F) = BYTE F T F T T F F T) /\
  (GF256_by_13 (BYTE F T F F F T F T) = BYTE F T F T F T F F) /\
  (GF256_by_13 (BYTE F T F F F T T F) = BYTE F T F F F F T T) /\
  (GF256_by_13 (BYTE F T F F F T T T) = BYTE F T F F T T T F) /\
  (GF256_by_13 (BYTE F T F F T F F F) = BYTE F F F F F T F T) /\
  (GF256_by_13 (BYTE F T F F T F F T) = BYTE F F F F T F F F) /\
  (GF256_by_13 (BYTE F T F F T F T F) = BYTE F F F T T T T T) /\
  (GF256_by_13 (BYTE F T F F T F T T) = BYTE F F F T F F T F) /\
  (GF256_by_13 (BYTE F T F F T T F F) = BYTE F F T T F F F T) /\
  (GF256_by_13 (BYTE F T F F T T F T) = BYTE F F T T T T F F) /\
  (GF256_by_13 (BYTE F T F F T T T F) = BYTE F F T F T F T T) /\
  (GF256_by_13 (BYTE F T F F T T T T) = BYTE F F T F F T T F) /\
  (GF256_by_13 (BYTE F T F T F F F F) = BYTE T F T T T T F T) /\
  (GF256_by_13 (BYTE F T F T F F F T) = BYTE T F T T F F F F) /\
  (GF256_by_13 (BYTE F T F T F F T F) = BYTE T F T F F T T T) /\
  (GF256_by_13 (BYTE F T F T F F T T) = BYTE T F T F T F T F) /\
  (GF256_by_13 (BYTE F T F T F T F F) = BYTE T F F F T F F T) /\
  (GF256_by_13 (BYTE F T F T F T F T) = BYTE T F F F F T F F) /\
  (GF256_by_13 (BYTE F T F T F T T F) = BYTE T F F T F F T T) /\
  (GF256_by_13 (BYTE F T F T F T T T) = BYTE T F F T T T T F) /\
  (GF256_by_13 (BYTE F T F T T F F F) = BYTE T T F T F T F T) /\
  (GF256_by_13 (BYTE F T F T T F F T) = BYTE T T F T T F F F) /\
  (GF256_by_13 (BYTE F T F T T F T F) = BYTE T T F F T T T T) /\
  (GF256_by_13 (BYTE F T F T T F T T) = BYTE T T F F F F T F) /\
  (GF256_by_13 (BYTE F T F T T T F F) = BYTE T T T F F F F T) /\
  (GF256_by_13 (BYTE F T F T T T F T) = BYTE T T T F T T F F) /\
  (GF256_by_13 (BYTE F T F T T T T F) = BYTE T T T T T F T T) /\
  (GF256_by_13 (BYTE F T F T T T T T) = BYTE T T T T F T T F) /\
  (GF256_by_13 (BYTE F T T F F F F F) = BYTE T T F T F T T F) /\
  (GF256_by_13 (BYTE F T T F F F F T) = BYTE T T F T T F T T) /\
  (GF256_by_13 (BYTE F T T F F F T F) = BYTE T T F F T T F F) /\
  (GF256_by_13 (BYTE F T T F F F T T) = BYTE T T F F F F F T) /\
  (GF256_by_13 (BYTE F T T F F T F F) = BYTE T T T F F F T F) /\
  (GF256_by_13 (BYTE F T T F F T F T) = BYTE T T T F T T T T) /\
  (GF256_by_13 (BYTE F T T F F T T F) = BYTE T T T T T F F F) /\
  (GF256_by_13 (BYTE F T T F F T T T) = BYTE T T T T F T F T) /\
  (GF256_by_13 (BYTE F T T F T F F F) = BYTE T F T T T T T F) /\
  (GF256_by_13 (BYTE F T T F T F F T) = BYTE T F T T F F T T) /\
  (GF256_by_13 (BYTE F T T F T F T F) = BYTE T F T F F T F F) /\
  (GF256_by_13 (BYTE F T T F T F T T) = BYTE T F T F T F F T) /\
  (GF256_by_13 (BYTE F T T F T T F F) = BYTE T F F F T F T F) /\
  (GF256_by_13 (BYTE F T T F T T F T) = BYTE T F F F F T T T) /\
  (GF256_by_13 (BYTE F T T F T T T F) = BYTE T F F T F F F F) /\
  (GF256_by_13 (BYTE F T T F T T T T) = BYTE T F F T T T F T) /\
  (GF256_by_13 (BYTE F T T T F F F F) = BYTE F F F F F T T F) /\
  (GF256_by_13 (BYTE F T T T F F F T) = BYTE F F F F T F T T) /\
  (GF256_by_13 (BYTE F T T T F F T F) = BYTE F F F T T T F F) /\
  (GF256_by_13 (BYTE F T T T F F T T) = BYTE F F F T F F F T) /\
  (GF256_by_13 (BYTE F T T T F T F F) = BYTE F F T T F F T F) /\
  (GF256_by_13 (BYTE F T T T F T F T) = BYTE F F T T T T T T) /\
  (GF256_by_13 (BYTE F T T T F T T F) = BYTE F F T F T F F F) /\
  (GF256_by_13 (BYTE F T T T F T T T) = BYTE F F T F F T F T) /\
  (GF256_by_13 (BYTE F T T T T F F F) = BYTE F T T F T T T F) /\
  (GF256_by_13 (BYTE F T T T T F F T) = BYTE F T T F F F T T) /\
  (GF256_by_13 (BYTE F T T T T F T F) = BYTE F T T T F T F F) /\
  (GF256_by_13 (BYTE F T T T T F T T) = BYTE F T T T T F F T) /\
  (GF256_by_13 (BYTE F T T T T T F F) = BYTE F T F T T F T F) /\
  (GF256_by_13 (BYTE F T T T T T F T) = BYTE F T F T F T T T) /\
  (GF256_by_13 (BYTE F T T T T T T F) = BYTE F T F F F F F F) /\
  (GF256_by_13 (BYTE F T T T T T T T) = BYTE F T F F T T F T) /\
  (GF256_by_13 (BYTE T F F F F F F F) = BYTE T T F T T F T F) /\
  (GF256_by_13 (BYTE T F F F F F F T) = BYTE T T F T F T T T) /\
  (GF256_by_13 (BYTE T F F F F F T F) = BYTE T T F F F F F F) /\
  (GF256_by_13 (BYTE T F F F F F T T) = BYTE T T F F T T F T) /\
  (GF256_by_13 (BYTE T F F F F T F F) = BYTE T T T F T T T F) /\
  (GF256_by_13 (BYTE T F F F F T F T) = BYTE T T T F F F T T) /\
  (GF256_by_13 (BYTE T F F F F T T F) = BYTE T T T T F T F F) /\
  (GF256_by_13 (BYTE T F F F F T T T) = BYTE T T T T T F F T) /\
  (GF256_by_13 (BYTE T F F F T F F F) = BYTE T F T T F F T F) /\
  (GF256_by_13 (BYTE T F F F T F F T) = BYTE T F T T T T T T) /\
  (GF256_by_13 (BYTE T F F F T F T F) = BYTE T F T F T F F F) /\
  (GF256_by_13 (BYTE T F F F T F T T) = BYTE T F T F F T F T) /\
  (GF256_by_13 (BYTE T F F F T T F F) = BYTE T F F F F T T F) /\
  (GF256_by_13 (BYTE T F F F T T F T) = BYTE T F F F T F T T) /\
  (GF256_by_13 (BYTE T F F F T T T F) = BYTE T F F T T T F F) /\
  (GF256_by_13 (BYTE T F F F T T T T) = BYTE T F F T F F F T) /\
  (GF256_by_13 (BYTE T F F T F F F F) = BYTE F F F F T F T F) /\
  (GF256_by_13 (BYTE T F F T F F F T) = BYTE F F F F F T T T) /\
  (GF256_by_13 (BYTE T F F T F F T F) = BYTE F F F T F F F F) /\
  (GF256_by_13 (BYTE T F F T F F T T) = BYTE F F F T T T F T) /\
  (GF256_by_13 (BYTE T F F T F T F F) = BYTE F F T T T T T F) /\
  (GF256_by_13 (BYTE T F F T F T F T) = BYTE F F T T F F T T) /\
  (GF256_by_13 (BYTE T F F T F T T F) = BYTE F F T F F T F F) /\
  (GF256_by_13 (BYTE T F F T F T T T) = BYTE F F T F T F F T) /\
  (GF256_by_13 (BYTE T F F T T F F F) = BYTE F T T F F F T F) /\
  (GF256_by_13 (BYTE T F F T T F F T) = BYTE F T T F T T T T) /\
  (GF256_by_13 (BYTE T F F T T F T F) = BYTE F T T T T F F F) /\
  (GF256_by_13 (BYTE T F F T T F T T) = BYTE F T T T F T F T) /\
  (GF256_by_13 (BYTE T F F T T T F F) = BYTE F T F T F T T F) /\
  (GF256_by_13 (BYTE T F F T T T F T) = BYTE F T F T T F T T) /\
  (GF256_by_13 (BYTE T F F T T T T F) = BYTE F T F F T T F F) /\
  (GF256_by_13 (BYTE T F F T T T T T) = BYTE F T F F F F F T) /\
  (GF256_by_13 (BYTE T F T F F F F F) = BYTE F T T F F F F T) /\
  (GF256_by_13 (BYTE T F T F F F F T) = BYTE F T T F T T F F) /\
  (GF256_by_13 (BYTE T F T F F F T F) = BYTE F T T T T F T T) /\
  (GF256_by_13 (BYTE T F T F F F T T) = BYTE F T T T F T T F) /\
  (GF256_by_13 (BYTE T F T F F T F F) = BYTE F T F T F T F T) /\
  (GF256_by_13 (BYTE T F T F F T F T) = BYTE F T F T T F F F) /\
  (GF256_by_13 (BYTE T F T F F T T F) = BYTE F T F F T T T T) /\
  (GF256_by_13 (BYTE T F T F F T T T) = BYTE F T F F F F T F) /\
  (GF256_by_13 (BYTE T F T F T F F F) = BYTE F F F F T F F T) /\
  (GF256_by_13 (BYTE T F T F T F F T) = BYTE F F F F F T F F) /\
  (GF256_by_13 (BYTE T F T F T F T F) = BYTE F F F T F F T T) /\
  (GF256_by_13 (BYTE T F T F T F T T) = BYTE F F F T T T T F) /\
  (GF256_by_13 (BYTE T F T F T T F F) = BYTE F F T T T T F T) /\
  (GF256_by_13 (BYTE T F T F T T F T) = BYTE F F T T F F F F) /\
  (GF256_by_13 (BYTE T F T F T T T F) = BYTE F F T F F T T T) /\
  (GF256_by_13 (BYTE T F T F T T T T) = BYTE F F T F T F T F) /\
  (GF256_by_13 (BYTE T F T T F F F F) = BYTE T F T T F F F T) /\
  (GF256_by_13 (BYTE T F T T F F F T) = BYTE T F T T T T F F) /\
  (GF256_by_13 (BYTE T F T T F F T F) = BYTE T F T F T F T T) /\
  (GF256_by_13 (BYTE T F T T F F T T) = BYTE T F T F F T T F) /\
  (GF256_by_13 (BYTE T F T T F T F F) = BYTE T F F F F T F T) /\
  (GF256_by_13 (BYTE T F T T F T F T) = BYTE T F F F T F F F) /\
  (GF256_by_13 (BYTE T F T T F T T F) = BYTE T F F T T T T T) /\
  (GF256_by_13 (BYTE T F T T F T T T) = BYTE T F F T F F T F) /\
  (GF256_by_13 (BYTE T F T T T F F F) = BYTE T T F T T F F T) /\
  (GF256_by_13 (BYTE T F T T T F F T) = BYTE T T F T F T F F) /\
  (GF256_by_13 (BYTE T F T T T F T F) = BYTE T T F F F F T T) /\
  (GF256_by_13 (BYTE T F T T T F T T) = BYTE T T F F T T T F) /\
  (GF256_by_13 (BYTE T F T T T T F F) = BYTE T T T F T T F T) /\
  (GF256_by_13 (BYTE T F T T T T F T) = BYTE T T T F F F F F) /\
  (GF256_by_13 (BYTE T F T T T T T F) = BYTE T T T T F T T T) /\
  (GF256_by_13 (BYTE T F T T T T T T) = BYTE T T T T T F T F) /\
  (GF256_by_13 (BYTE T T F F F F F F) = BYTE T F T T F T T T) /\
  (GF256_by_13 (BYTE T T F F F F F T) = BYTE T F T T T F T F) /\
  (GF256_by_13 (BYTE T T F F F F T F) = BYTE T F T F T T F T) /\
  (GF256_by_13 (BYTE T T F F F F T T) = BYTE T F T F F F F F) /\
  (GF256_by_13 (BYTE T T F F F T F F) = BYTE T F F F F F T T) /\
  (GF256_by_13 (BYTE T T F F F T F T) = BYTE T F F F T T T F) /\
  (GF256_by_13 (BYTE T T F F F T T F) = BYTE T F F T T F F T) /\
  (GF256_by_13 (BYTE T T F F F T T T) = BYTE T F F T F T F F) /\
  (GF256_by_13 (BYTE T T F F T F F F) = BYTE T T F T T T T T) /\
  (GF256_by_13 (BYTE T T F F T F F T) = BYTE T T F T F F T F) /\
  (GF256_by_13 (BYTE T T F F T F T F) = BYTE T T F F F T F T) /\
  (GF256_by_13 (BYTE T T F F T F T T) = BYTE T T F F T F F F) /\
  (GF256_by_13 (BYTE T T F F T T F F) = BYTE T T T F T F T T) /\
  (GF256_by_13 (BYTE T T F F T T F T) = BYTE T T T F F T T F) /\
  (GF256_by_13 (BYTE T T F F T T T F) = BYTE T T T T F F F T) /\
  (GF256_by_13 (BYTE T T F F T T T T) = BYTE T T T T T T F F) /\
  (GF256_by_13 (BYTE T T F T F F F F) = BYTE F T T F F T T T) /\
  (GF256_by_13 (BYTE T T F T F F F T) = BYTE F T T F T F T F) /\
  (GF256_by_13 (BYTE T T F T F F T F) = BYTE F T T T T T F T) /\
  (GF256_by_13 (BYTE T T F T F F T T) = BYTE F T T T F F F F) /\
  (GF256_by_13 (BYTE T T F T F T F F) = BYTE F T F T F F T T) /\
  (GF256_by_13 (BYTE T T F T F T F T) = BYTE F T F T T T T F) /\
  (GF256_by_13 (BYTE T T F T F T T F) = BYTE F T F F T F F T) /\
  (GF256_by_13 (BYTE T T F T F T T T) = BYTE F T F F F T F F) /\
  (GF256_by_13 (BYTE T T F T T F F F) = BYTE F F F F T T T T) /\
  (GF256_by_13 (BYTE T T F T T F F T) = BYTE F F F F F F T F) /\
  (GF256_by_13 (BYTE T T F T T F T F) = BYTE F F F T F T F T) /\
  (GF256_by_13 (BYTE T T F T T F T T) = BYTE F F F T T F F F) /\
  (GF256_by_13 (BYTE T T F T T T F F) = BYTE F F T T T F T T) /\
  (GF256_by_13 (BYTE T T F T T T F T) = BYTE F F T T F T T F) /\
  (GF256_by_13 (BYTE T T F T T T T F) = BYTE F F T F F F F T) /\
  (GF256_by_13 (BYTE T T F T T T T T) = BYTE F F T F T T F F) /\
  (GF256_by_13 (BYTE T T T F F F F F) = BYTE F F F F T T F F) /\
  (GF256_by_13 (BYTE T T T F F F F T) = BYTE F F F F F F F T) /\
  (GF256_by_13 (BYTE T T T F F F T F) = BYTE F F F T F T T F) /\
  (GF256_by_13 (BYTE T T T F F F T T) = BYTE F F F T T F T T) /\
  (GF256_by_13 (BYTE T T T F F T F F) = BYTE F F T T T F F F) /\
  (GF256_by_13 (BYTE T T T F F T F T) = BYTE F F T T F T F T) /\
  (GF256_by_13 (BYTE T T T F F T T F) = BYTE F F T F F F T F) /\
  (GF256_by_13 (BYTE T T T F F T T T) = BYTE F F T F T T T T) /\
  (GF256_by_13 (BYTE T T T F T F F F) = BYTE F T T F F T F F) /\
  (GF256_by_13 (BYTE T T T F T F F T) = BYTE F T T F T F F T) /\
  (GF256_by_13 (BYTE T T T F T F T F) = BYTE F T T T T T T F) /\
  (GF256_by_13 (BYTE T T T F T F T T) = BYTE F T T T F F T T) /\
  (GF256_by_13 (BYTE T T T F T T F F) = BYTE F T F T F F F F) /\
  (GF256_by_13 (BYTE T T T F T T F T) = BYTE F T F T T T F T) /\
  (GF256_by_13 (BYTE T T T F T T T F) = BYTE F T F F T F T F) /\
  (GF256_by_13 (BYTE T T T F T T T T) = BYTE F T F F F T T T) /\
  (GF256_by_13 (BYTE T T T T F F F F) = BYTE T T F T T T F F) /\
  (GF256_by_13 (BYTE T T T T F F F T) = BYTE T T F T F F F T) /\
  (GF256_by_13 (BYTE T T T T F F T F) = BYTE T T F F F T T F) /\
  (GF256_by_13 (BYTE T T T T F F T T) = BYTE T T F F T F T T) /\
  (GF256_by_13 (BYTE T T T T F T F F) = BYTE T T T F T F F F) /\
  (GF256_by_13 (BYTE T T T T F T F T) = BYTE T T T F F T F T) /\
  (GF256_by_13 (BYTE T T T T F T T F) = BYTE T T T T F F T F) /\
  (GF256_by_13 (BYTE T T T T F T T T) = BYTE T T T T T T T T) /\
  (GF256_by_13 (BYTE T T T T T F F F) = BYTE T F T T F T F F) /\
  (GF256_by_13 (BYTE T T T T T F F T) = BYTE T F T T T F F T) /\
  (GF256_by_13 (BYTE T T T T T F T F) = BYTE T F T F T T T F) /\
  (GF256_by_13 (BYTE T T T T T F T T) = BYTE T F T F F F T T) /\
  (GF256_by_13 (BYTE T T T T T T F F) = BYTE T F F F F F F F) /\
  (GF256_by_13 (BYTE T T T T T T F T) = BYTE T F F F T T F T) /\
  (GF256_by_13 (BYTE T T T T T T T F) = BYTE T F F T T F T F) /\
  (GF256_by_13 (BYTE T T T T T T T T) = BYTE T F F T F T T T)`;

val GF256_by_14_def = Count.apply Define
 `(GF256_by_14 (BYTE F F F F F F F F) = BYTE F F F F F F F F) /\
  (GF256_by_14 (BYTE F F F F F F F T) = BYTE F F F F T T T F) /\
  (GF256_by_14 (BYTE F F F F F F T F) = BYTE F F F T T T F F) /\
  (GF256_by_14 (BYTE F F F F F F T T) = BYTE F F F T F F T F) /\
  (GF256_by_14 (BYTE F F F F F T F F) = BYTE F F T T T F F F) /\
  (GF256_by_14 (BYTE F F F F F T F T) = BYTE F F T T F T T F) /\
  (GF256_by_14 (BYTE F F F F F T T F) = BYTE F F T F F T F F) /\
  (GF256_by_14 (BYTE F F F F F T T T) = BYTE F F T F T F T F) /\
  (GF256_by_14 (BYTE F F F F T F F F) = BYTE F T T T F F F F) /\
  (GF256_by_14 (BYTE F F F F T F F T) = BYTE F T T T T T T F) /\
  (GF256_by_14 (BYTE F F F F T F T F) = BYTE F T T F T T F F) /\
  (GF256_by_14 (BYTE F F F F T F T T) = BYTE F T T F F F T F) /\
  (GF256_by_14 (BYTE F F F F T T F F) = BYTE F T F F T F F F) /\
  (GF256_by_14 (BYTE F F F F T T F T) = BYTE F T F F F T T F) /\
  (GF256_by_14 (BYTE F F F F T T T F) = BYTE F T F T F T F F) /\
  (GF256_by_14 (BYTE F F F F T T T T) = BYTE F T F T T F T F) /\
  (GF256_by_14 (BYTE F F F T F F F F) = BYTE T T T F F F F F) /\
  (GF256_by_14 (BYTE F F F T F F F T) = BYTE T T T F T T T F) /\
  (GF256_by_14 (BYTE F F F T F F T F) = BYTE T T T T T T F F) /\
  (GF256_by_14 (BYTE F F F T F F T T) = BYTE T T T T F F T F) /\
  (GF256_by_14 (BYTE F F F T F T F F) = BYTE T T F T T F F F) /\
  (GF256_by_14 (BYTE F F F T F T F T) = BYTE T T F T F T T F) /\
  (GF256_by_14 (BYTE F F F T F T T F) = BYTE T T F F F T F F) /\
  (GF256_by_14 (BYTE F F F T F T T T) = BYTE T T F F T F T F) /\
  (GF256_by_14 (BYTE F F F T T F F F) = BYTE T F F T F F F F) /\
  (GF256_by_14 (BYTE F F F T T F F T) = BYTE T F F T T T T F) /\
  (GF256_by_14 (BYTE F F F T T F T F) = BYTE T F F F T T F F) /\
  (GF256_by_14 (BYTE F F F T T F T T) = BYTE T F F F F F T F) /\
  (GF256_by_14 (BYTE F F F T T T F F) = BYTE T F T F T F F F) /\
  (GF256_by_14 (BYTE F F F T T T F T) = BYTE T F T F F T T F) /\
  (GF256_by_14 (BYTE F F F T T T T F) = BYTE T F T T F T F F) /\
  (GF256_by_14 (BYTE F F F T T T T T) = BYTE T F T T T F T F) /\
  (GF256_by_14 (BYTE F F T F F F F F) = BYTE T T F T T F T T) /\
  (GF256_by_14 (BYTE F F T F F F F T) = BYTE T T F T F T F T) /\
  (GF256_by_14 (BYTE F F T F F F T F) = BYTE T T F F F T T T) /\
  (GF256_by_14 (BYTE F F T F F F T T) = BYTE T T F F T F F T) /\
  (GF256_by_14 (BYTE F F T F F T F F) = BYTE T T T F F F T T) /\
  (GF256_by_14 (BYTE F F T F F T F T) = BYTE T T T F T T F T) /\
  (GF256_by_14 (BYTE F F T F F T T F) = BYTE T T T T T T T T) /\
  (GF256_by_14 (BYTE F F T F F T T T) = BYTE T T T T F F F T) /\
  (GF256_by_14 (BYTE F F T F T F F F) = BYTE T F T F T F T T) /\
  (GF256_by_14 (BYTE F F T F T F F T) = BYTE T F T F F T F T) /\
  (GF256_by_14 (BYTE F F T F T F T F) = BYTE T F T T F T T T) /\
  (GF256_by_14 (BYTE F F T F T F T T) = BYTE T F T T T F F T) /\
  (GF256_by_14 (BYTE F F T F T T F F) = BYTE T F F T F F T T) /\
  (GF256_by_14 (BYTE F F T F T T F T) = BYTE T F F T T T F T) /\
  (GF256_by_14 (BYTE F F T F T T T F) = BYTE T F F F T T T T) /\
  (GF256_by_14 (BYTE F F T F T T T T) = BYTE T F F F F F F T) /\
  (GF256_by_14 (BYTE F F T T F F F F) = BYTE F F T T T F T T) /\
  (GF256_by_14 (BYTE F F T T F F F T) = BYTE F F T T F T F T) /\
  (GF256_by_14 (BYTE F F T T F F T F) = BYTE F F T F F T T T) /\
  (GF256_by_14 (BYTE F F T T F F T T) = BYTE F F T F T F F T) /\
  (GF256_by_14 (BYTE F F T T F T F F) = BYTE F F F F F F T T) /\
  (GF256_by_14 (BYTE F F T T F T F T) = BYTE F F F F T T F T) /\
  (GF256_by_14 (BYTE F F T T F T T F) = BYTE F F F T T T T T) /\
  (GF256_by_14 (BYTE F F T T F T T T) = BYTE F F F T F F F T) /\
  (GF256_by_14 (BYTE F F T T T F F F) = BYTE F T F F T F T T) /\
  (GF256_by_14 (BYTE F F T T T F F T) = BYTE F T F F F T F T) /\
  (GF256_by_14 (BYTE F F T T T F T F) = BYTE F T F T F T T T) /\
  (GF256_by_14 (BYTE F F T T T F T T) = BYTE F T F T T F F T) /\
  (GF256_by_14 (BYTE F F T T T T F F) = BYTE F T T T F F T T) /\
  (GF256_by_14 (BYTE F F T T T T F T) = BYTE F T T T T T F T) /\
  (GF256_by_14 (BYTE F F T T T T T F) = BYTE F T T F T T T T) /\
  (GF256_by_14 (BYTE F F T T T T T T) = BYTE F T T F F F F T) /\
  (GF256_by_14 (BYTE F T F F F F F F) = BYTE T F T F T T F T) /\
  (GF256_by_14 (BYTE F T F F F F F T) = BYTE T F T F F F T T) /\
  (GF256_by_14 (BYTE F T F F F F T F) = BYTE T F T T F F F T) /\
  (GF256_by_14 (BYTE F T F F F F T T) = BYTE T F T T T T T T) /\
  (GF256_by_14 (BYTE F T F F F T F F) = BYTE T F F T F T F T) /\
  (GF256_by_14 (BYTE F T F F F T F T) = BYTE T F F T T F T T) /\
  (GF256_by_14 (BYTE F T F F F T T F) = BYTE T F F F T F F T) /\
  (GF256_by_14 (BYTE F T F F F T T T) = BYTE T F F F F T T T) /\
  (GF256_by_14 (BYTE F T F F T F F F) = BYTE T T F T T T F T) /\
  (GF256_by_14 (BYTE F T F F T F F T) = BYTE T T F T F F T T) /\
  (GF256_by_14 (BYTE F T F F T F T F) = BYTE T T F F F F F T) /\
  (GF256_by_14 (BYTE F T F F T F T T) = BYTE T T F F T T T T) /\
  (GF256_by_14 (BYTE F T F F T T F F) = BYTE T T T F F T F T) /\
  (GF256_by_14 (BYTE F T F F T T F T) = BYTE T T T F T F T T) /\
  (GF256_by_14 (BYTE F T F F T T T F) = BYTE T T T T T F F T) /\
  (GF256_by_14 (BYTE F T F F T T T T) = BYTE T T T T F T T T) /\
  (GF256_by_14 (BYTE F T F T F F F F) = BYTE F T F F T T F T) /\
  (GF256_by_14 (BYTE F T F T F F F T) = BYTE F T F F F F T T) /\
  (GF256_by_14 (BYTE F T F T F F T F) = BYTE F T F T F F F T) /\
  (GF256_by_14 (BYTE F T F T F F T T) = BYTE F T F T T T T T) /\
  (GF256_by_14 (BYTE F T F T F T F F) = BYTE F T T T F T F T) /\
  (GF256_by_14 (BYTE F T F T F T F T) = BYTE F T T T T F T T) /\
  (GF256_by_14 (BYTE F T F T F T T F) = BYTE F T T F T F F T) /\
  (GF256_by_14 (BYTE F T F T F T T T) = BYTE F T T F F T T T) /\
  (GF256_by_14 (BYTE F T F T T F F F) = BYTE F F T T T T F T) /\
  (GF256_by_14 (BYTE F T F T T F F T) = BYTE F F T T F F T T) /\
  (GF256_by_14 (BYTE F T F T T F T F) = BYTE F F T F F F F T) /\
  (GF256_by_14 (BYTE F T F T T F T T) = BYTE F F T F T T T T) /\
  (GF256_by_14 (BYTE F T F T T T F F) = BYTE F F F F F T F T) /\
  (GF256_by_14 (BYTE F T F T T T F T) = BYTE F F F F T F T T) /\
  (GF256_by_14 (BYTE F T F T T T T F) = BYTE F F F T T F F T) /\
  (GF256_by_14 (BYTE F T F T T T T T) = BYTE F F F T F T T T) /\
  (GF256_by_14 (BYTE F T T F F F F F) = BYTE F T T T F T T F) /\
  (GF256_by_14 (BYTE F T T F F F F T) = BYTE F T T T T F F F) /\
  (GF256_by_14 (BYTE F T T F F F T F) = BYTE F T T F T F T F) /\
  (GF256_by_14 (BYTE F T T F F F T T) = BYTE F T T F F T F F) /\
  (GF256_by_14 (BYTE F T T F F T F F) = BYTE F T F F T T T F) /\
  (GF256_by_14 (BYTE F T T F F T F T) = BYTE F T F F F F F F) /\
  (GF256_by_14 (BYTE F T T F F T T F) = BYTE F T F T F F T F) /\
  (GF256_by_14 (BYTE F T T F F T T T) = BYTE F T F T T T F F) /\
  (GF256_by_14 (BYTE F T T F T F F F) = BYTE F F F F F T T F) /\
  (GF256_by_14 (BYTE F T T F T F F T) = BYTE F F F F T F F F) /\
  (GF256_by_14 (BYTE F T T F T F T F) = BYTE F F F T T F T F) /\
  (GF256_by_14 (BYTE F T T F T F T T) = BYTE F F F T F T F F) /\
  (GF256_by_14 (BYTE F T T F T T F F) = BYTE F F T T T T T F) /\
  (GF256_by_14 (BYTE F T T F T T F T) = BYTE F F T T F F F F) /\
  (GF256_by_14 (BYTE F T T F T T T F) = BYTE F F T F F F T F) /\
  (GF256_by_14 (BYTE F T T F T T T T) = BYTE F F T F T T F F) /\
  (GF256_by_14 (BYTE F T T T F F F F) = BYTE T F F T F T T F) /\
  (GF256_by_14 (BYTE F T T T F F F T) = BYTE T F F T T F F F) /\
  (GF256_by_14 (BYTE F T T T F F T F) = BYTE T F F F T F T F) /\
  (GF256_by_14 (BYTE F T T T F F T T) = BYTE T F F F F T F F) /\
  (GF256_by_14 (BYTE F T T T F T F F) = BYTE T F T F T T T F) /\
  (GF256_by_14 (BYTE F T T T F T F T) = BYTE T F T F F F F F) /\
  (GF256_by_14 (BYTE F T T T F T T F) = BYTE T F T T F F T F) /\
  (GF256_by_14 (BYTE F T T T F T T T) = BYTE T F T T T T F F) /\
  (GF256_by_14 (BYTE F T T T T F F F) = BYTE T T T F F T T F) /\
  (GF256_by_14 (BYTE F T T T T F F T) = BYTE T T T F T F F F) /\
  (GF256_by_14 (BYTE F T T T T F T F) = BYTE T T T T T F T F) /\
  (GF256_by_14 (BYTE F T T T T F T T) = BYTE T T T T F T F F) /\
  (GF256_by_14 (BYTE F T T T T T F F) = BYTE T T F T T T T F) /\
  (GF256_by_14 (BYTE F T T T T T F T) = BYTE T T F T F F F F) /\
  (GF256_by_14 (BYTE F T T T T T T F) = BYTE T T F F F F T F) /\
  (GF256_by_14 (BYTE F T T T T T T T) = BYTE T T F F T T F F) /\
  (GF256_by_14 (BYTE T F F F F F F F) = BYTE F T F F F F F T) /\
  (GF256_by_14 (BYTE T F F F F F F T) = BYTE F T F F T T T T) /\
  (GF256_by_14 (BYTE T F F F F F T F) = BYTE F T F T T T F T) /\
  (GF256_by_14 (BYTE T F F F F F T T) = BYTE F T F T F F T T) /\
  (GF256_by_14 (BYTE T F F F F T F F) = BYTE F T T T T F F T) /\
  (GF256_by_14 (BYTE T F F F F T F T) = BYTE F T T T F T T T) /\
  (GF256_by_14 (BYTE T F F F F T T F) = BYTE F T T F F T F T) /\
  (GF256_by_14 (BYTE T F F F F T T T) = BYTE F T T F T F T T) /\
  (GF256_by_14 (BYTE T F F F T F F F) = BYTE F F T T F F F T) /\
  (GF256_by_14 (BYTE T F F F T F F T) = BYTE F F T T T T T T) /\
  (GF256_by_14 (BYTE T F F F T F T F) = BYTE F F T F T T F T) /\
  (GF256_by_14 (BYTE T F F F T F T T) = BYTE F F T F F F T T) /\
  (GF256_by_14 (BYTE T F F F T T F F) = BYTE F F F F T F F T) /\
  (GF256_by_14 (BYTE T F F F T T F T) = BYTE F F F F F T T T) /\
  (GF256_by_14 (BYTE T F F F T T T F) = BYTE F F F T F T F T) /\
  (GF256_by_14 (BYTE T F F F T T T T) = BYTE F F F T T F T T) /\
  (GF256_by_14 (BYTE T F F T F F F F) = BYTE T F T F F F F T) /\
  (GF256_by_14 (BYTE T F F T F F F T) = BYTE T F T F T T T T) /\
  (GF256_by_14 (BYTE T F F T F F T F) = BYTE T F T T T T F T) /\
  (GF256_by_14 (BYTE T F F T F F T T) = BYTE T F T T F F T T) /\
  (GF256_by_14 (BYTE T F F T F T F F) = BYTE T F F T T F F T) /\
  (GF256_by_14 (BYTE T F F T F T F T) = BYTE T F F T F T T T) /\
  (GF256_by_14 (BYTE T F F T F T T F) = BYTE T F F F F T F T) /\
  (GF256_by_14 (BYTE T F F T F T T T) = BYTE T F F F T F T T) /\
  (GF256_by_14 (BYTE T F F T T F F F) = BYTE T T F T F F F T) /\
  (GF256_by_14 (BYTE T F F T T F F T) = BYTE T T F T T T T T) /\
  (GF256_by_14 (BYTE T F F T T F T F) = BYTE T T F F T T F T) /\
  (GF256_by_14 (BYTE T F F T T F T T) = BYTE T T F F F F T T) /\
  (GF256_by_14 (BYTE T F F T T T F F) = BYTE T T T F T F F T) /\
  (GF256_by_14 (BYTE T F F T T T F T) = BYTE T T T F F T T T) /\
  (GF256_by_14 (BYTE T F F T T T T F) = BYTE T T T T F T F T) /\
  (GF256_by_14 (BYTE T F F T T T T T) = BYTE T T T T T F T T) /\
  (GF256_by_14 (BYTE T F T F F F F F) = BYTE T F F T T F T F) /\
  (GF256_by_14 (BYTE T F T F F F F T) = BYTE T F F T F T F F) /\
  (GF256_by_14 (BYTE T F T F F F T F) = BYTE T F F F F T T F) /\
  (GF256_by_14 (BYTE T F T F F F T T) = BYTE T F F F T F F F) /\
  (GF256_by_14 (BYTE T F T F F T F F) = BYTE T F T F F F T F) /\
  (GF256_by_14 (BYTE T F T F F T F T) = BYTE T F T F T T F F) /\
  (GF256_by_14 (BYTE T F T F F T T F) = BYTE T F T T T T T F) /\
  (GF256_by_14 (BYTE T F T F F T T T) = BYTE T F T T F F F F) /\
  (GF256_by_14 (BYTE T F T F T F F F) = BYTE T T T F T F T F) /\
  (GF256_by_14 (BYTE T F T F T F F T) = BYTE T T T F F T F F) /\
  (GF256_by_14 (BYTE T F T F T F T F) = BYTE T T T T F T T F) /\
  (GF256_by_14 (BYTE T F T F T F T T) = BYTE T T T T T F F F) /\
  (GF256_by_14 (BYTE T F T F T T F F) = BYTE T T F T F F T F) /\
  (GF256_by_14 (BYTE T F T F T T F T) = BYTE T T F T T T F F) /\
  (GF256_by_14 (BYTE T F T F T T T F) = BYTE T T F F T T T F) /\
  (GF256_by_14 (BYTE T F T F T T T T) = BYTE T T F F F F F F) /\
  (GF256_by_14 (BYTE T F T T F F F F) = BYTE F T T T T F T F) /\
  (GF256_by_14 (BYTE T F T T F F F T) = BYTE F T T T F T F F) /\
  (GF256_by_14 (BYTE T F T T F F T F) = BYTE F T T F F T T F) /\
  (GF256_by_14 (BYTE T F T T F F T T) = BYTE F T T F T F F F) /\
  (GF256_by_14 (BYTE T F T T F T F F) = BYTE F T F F F F T F) /\
  (GF256_by_14 (BYTE T F T T F T F T) = BYTE F T F F T T F F) /\
  (GF256_by_14 (BYTE T F T T F T T F) = BYTE F T F T T T T F) /\
  (GF256_by_14 (BYTE T F T T F T T T) = BYTE F T F T F F F F) /\
  (GF256_by_14 (BYTE T F T T T F F F) = BYTE F F F F T F T F) /\
  (GF256_by_14 (BYTE T F T T T F F T) = BYTE F F F F F T F F) /\
  (GF256_by_14 (BYTE T F T T T F T F) = BYTE F F F T F T T F) /\
  (GF256_by_14 (BYTE T F T T T F T T) = BYTE F F F T T F F F) /\
  (GF256_by_14 (BYTE T F T T T T F F) = BYTE F F T T F F T F) /\
  (GF256_by_14 (BYTE T F T T T T F T) = BYTE F F T T T T F F) /\
  (GF256_by_14 (BYTE T F T T T T T F) = BYTE F F T F T T T F) /\
  (GF256_by_14 (BYTE T F T T T T T T) = BYTE F F T F F F F F) /\
  (GF256_by_14 (BYTE T T F F F F F F) = BYTE T T T F T T F F) /\
  (GF256_by_14 (BYTE T T F F F F F T) = BYTE T T T F F F T F) /\
  (GF256_by_14 (BYTE T T F F F F T F) = BYTE T T T T F F F F) /\
  (GF256_by_14 (BYTE T T F F F F T T) = BYTE T T T T T T T F) /\
  (GF256_by_14 (BYTE T T F F F T F F) = BYTE T T F T F T F F) /\
  (GF256_by_14 (BYTE T T F F F T F T) = BYTE T T F T T F T F) /\
  (GF256_by_14 (BYTE T T F F F T T F) = BYTE T T F F T F F F) /\
  (GF256_by_14 (BYTE T T F F F T T T) = BYTE T T F F F T T F) /\
  (GF256_by_14 (BYTE T T F F T F F F) = BYTE T F F T T T F F) /\
  (GF256_by_14 (BYTE T T F F T F F T) = BYTE T F F T F F T F) /\
  (GF256_by_14 (BYTE T T F F T F T F) = BYTE T F F F F F F F) /\
  (GF256_by_14 (BYTE T T F F T F T T) = BYTE T F F F T T T F) /\
  (GF256_by_14 (BYTE T T F F T T F F) = BYTE T F T F F T F F) /\
  (GF256_by_14 (BYTE T T F F T T F T) = BYTE T F T F T F T F) /\
  (GF256_by_14 (BYTE T T F F T T T F) = BYTE T F T T T F F F) /\
  (GF256_by_14 (BYTE T T F F T T T T) = BYTE T F T T F T T F) /\
  (GF256_by_14 (BYTE T T F T F F F F) = BYTE F F F F T T F F) /\
  (GF256_by_14 (BYTE T T F T F F F T) = BYTE F F F F F F T F) /\
  (GF256_by_14 (BYTE T T F T F F T F) = BYTE F F F T F F F F) /\
  (GF256_by_14 (BYTE T T F T F F T T) = BYTE F F F T T T T F) /\
  (GF256_by_14 (BYTE T T F T F T F F) = BYTE F F T T F T F F) /\
  (GF256_by_14 (BYTE T T F T F T F T) = BYTE F F T T T F T F) /\
  (GF256_by_14 (BYTE T T F T F T T F) = BYTE F F T F T F F F) /\
  (GF256_by_14 (BYTE T T F T F T T T) = BYTE F F T F F T T F) /\
  (GF256_by_14 (BYTE T T F T T F F F) = BYTE F T T T T T F F) /\
  (GF256_by_14 (BYTE T T F T T F F T) = BYTE F T T T F F T F) /\
  (GF256_by_14 (BYTE T T F T T F T F) = BYTE F T T F F F F F) /\
  (GF256_by_14 (BYTE T T F T T F T T) = BYTE F T T F T T T F) /\
  (GF256_by_14 (BYTE T T F T T T F F) = BYTE F T F F F T F F) /\
  (GF256_by_14 (BYTE T T F T T T F T) = BYTE F T F F T F T F) /\
  (GF256_by_14 (BYTE T T F T T T T F) = BYTE F T F T T F F F) /\
  (GF256_by_14 (BYTE T T F T T T T T) = BYTE F T F T F T T F) /\
  (GF256_by_14 (BYTE T T T F F F F F) = BYTE F F T T F T T T) /\
  (GF256_by_14 (BYTE T T T F F F F T) = BYTE F F T T T F F T) /\
  (GF256_by_14 (BYTE T T T F F F T F) = BYTE F F T F T F T T) /\
  (GF256_by_14 (BYTE T T T F F F T T) = BYTE F F T F F T F T) /\
  (GF256_by_14 (BYTE T T T F F T F F) = BYTE F F F F T T T T) /\
  (GF256_by_14 (BYTE T T T F F T F T) = BYTE F F F F F F F T) /\
  (GF256_by_14 (BYTE T T T F F T T F) = BYTE F F F T F F T T) /\
  (GF256_by_14 (BYTE T T T F F T T T) = BYTE F F F T T T F T) /\
  (GF256_by_14 (BYTE T T T F T F F F) = BYTE F T F F F T T T) /\
  (GF256_by_14 (BYTE T T T F T F F T) = BYTE F T F F T F F T) /\
  (GF256_by_14 (BYTE T T T F T F T F) = BYTE F T F T T F T T) /\
  (GF256_by_14 (BYTE T T T F T F T T) = BYTE F T F T F T F T) /\
  (GF256_by_14 (BYTE T T T F T T F F) = BYTE F T T T T T T T) /\
  (GF256_by_14 (BYTE T T T F T T F T) = BYTE F T T T F F F T) /\
  (GF256_by_14 (BYTE T T T F T T T F) = BYTE F T T F F F T T) /\
  (GF256_by_14 (BYTE T T T F T T T T) = BYTE F T T F T T F T) /\
  (GF256_by_14 (BYTE T T T T F F F F) = BYTE T T F T F T T T) /\
  (GF256_by_14 (BYTE T T T T F F F T) = BYTE T T F T T F F T) /\
  (GF256_by_14 (BYTE T T T T F F T F) = BYTE T T F F T F T T) /\
  (GF256_by_14 (BYTE T T T T F F T T) = BYTE T T F F F T F T) /\
  (GF256_by_14 (BYTE T T T T F T F F) = BYTE T T T F T T T T) /\
  (GF256_by_14 (BYTE T T T T F T F T) = BYTE T T T F F F F T) /\
  (GF256_by_14 (BYTE T T T T F T T F) = BYTE T T T T F F T T) /\
  (GF256_by_14 (BYTE T T T T F T T T) = BYTE T T T T T T F T) /\
  (GF256_by_14 (BYTE T T T T T F F F) = BYTE T F T F F T T T) /\
  (GF256_by_14 (BYTE T T T T T F F T) = BYTE T F T F T F F T) /\
  (GF256_by_14 (BYTE T T T T T F T F) = BYTE T F T T T F T T) /\
  (GF256_by_14 (BYTE T T T T T F T T) = BYTE T F T T F T F T) /\
  (GF256_by_14 (BYTE T T T T T T F F) = BYTE T F F T T T T T) /\
  (GF256_by_14 (BYTE T T T T T T F T) = BYTE T F F T F F F T) /\
  (GF256_by_14 (BYTE T T T T T T T F) = BYTE T F F F F F T T) /\
  (GF256_by_14 (BYTE T T T T T T T T) = BYTE T F F F T T F T)`;

val Sbox_Inversion = Q.store_thm
("Sbox_Inversion",
 `!w:word8. InvSbox (Sbox w) = w`,
 SIMP_TAC std_ss [FORALL_BYTE_BITS, Sbox_def, InvSbox_def]);

val _ = export_theory();
